* various bug fix related to the environment returned when a match

[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 4dcc772975b9e28287d3840b90bd640de4a067cf..3622a8c921edf290ddd3d47051b08c89a73ce87a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -474,6 +474,10 @@ EXTEND
       DELIM "\\["; some = l2_pattern; DELIM "\\]";
       DELIM "\\["; none = l2_pattern; DELIM "\\]" ->
         Default (some, none)
+    | SYMBOL "\\IF";
+      DELIM "\\["; guard = l2_pattern; DELIM "\\]";
+      DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
+        If (guard, p)    
     ]
   ];
   l2_pattern: LEVEL "10"  (* let in *)