* implemented unless

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 3622a8c921edf290ddd3d47051b08c89a73ce87a..f3a6035d4c5d87918d63f3fe78cc1385434c27d6 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -478,6 +478,10 @@ EXTEND
       DELIM "\\["; guard = l2_pattern; DELIM "\\]";
       DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
         If (guard, p)    
+    | SYMBOL "\\UNLESS";
+      DELIM "\\["; guard = l2_pattern; DELIM "\\]";
+      DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
+        Unless (guard, p)        
     ]
   ];
   l2_pattern: LEVEL "10"  (* let in *)