Negation

spectec/doc/semantics/il/1-syntax.spectec

diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec
index e7d52be..add78f4 100644
--- a/spectec/doc/semantics/il/1-syntax.spectec
+++ b/spectec/doc/semantics/il/1-syntax.spectec
@@ -4,6 +4,8 @@
 def $with_polymorphic_types : bool
 def $with_dependent_types : bool
 def $with_family_types : bool
+def $with_negation : bool
+def $with_else : bool
 def $with_grammars : bool
 def $with_noncomputational : bool  ;; semantic restriction
 
@@ -186,8 +188,8 @@
 syntax prem =
   | REL id arg* `: exp              ;; can only occur in relations
   | IF exp
-  | ELSE
-  | NOT prem
+  | ELSE                            -- if $with_negation /\ $with_else
+  | NOT prem                        -- if $with_negation
   | LET exp `= exp                  ;; TODO: variables/quantifiers?
   | ITER prem iter exppull*