* 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 ba12b49da15fe86d2c2ceef0baac78d254180e2f..f3a6035d4c5d87918d63f3fe78cc1385434c27d6 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -474,6 +474,14 @@ 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)    
+    | SYMBOL "\\UNLESS";
+      DELIM "\\["; guard = l2_pattern; DELIM "\\]";
+      DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
+        Unless (guard, p)        
     ]
   ];
   l2_pattern: LEVEL "10"  (* let in *)
@@ -543,7 +551,7 @@ EXTEND
     ]
   ];
   level3_term: [
-    [ u = URI -> UriPattern u
+    [ u = URI -> UriPattern (UriManager.uri_of_string u)
     | id = IDENT -> VarPattern id
     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
         (match terms with