X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=5e70ff571ecd62b8a3402da395c8aebee9b5312a;hb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;hp=e1623f3d2bbcec6387f688798e5d253adb40af0d;hpb=7e7ce7bb6b95e9bd10dc180671ba7512ff2537dd;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e1623f3d2..5e70ff571 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -335,7 +335,8 @@ EXTEND
         TacticAst.Apply (loc, t)
     | [ IDENT "assumption" ] ->
         TacticAst.Assumption loc
-    | [ IDENT "auto" ] -> TacticAst.Auto loc
+    | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> 
+          TacticAst.Auto (loc,num)
     | [ IDENT "change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->
@@ -397,7 +398,10 @@ EXTEND
     | [ IDENT "replace" ];
       t1 = tactic_term; "with"; t2 = tactic_term ->
         TacticAst.Replace (loc, t1, t2)
-    (* TODO Rewrite *)
+    | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Left, t, None)
+    | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Right, t, None)
     (* TODO Replace_pattern *)
     | [ IDENT "right" ] -> TacticAst.Right loc
     | [ IDENT "ring" ] -> TacticAst.Ring loc
@@ -480,6 +484,16 @@ EXTEND
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
+    | [ IDENT "whelp"; "match" ] ; t = term -> 
+        TacticAst.WMatch (loc,t)
+    | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
+        TacticAst.WInstance (loc,t)
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+        TacticAst.WLocate (loc,id)
+    | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+        TacticAst.WElim (loc, t)
+    | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
+        TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];
 
@@ -557,12 +571,26 @@ EXTEND
         TacticAst.Alias (loc, spec)
   ]];
 
-  statement: [
+  executable: [
     [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
     | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
     | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
     ]
   ];
+  
+  comment: [
+    [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> 
+       TacticAst.Code (loc, ex)
+    | str = NOTE -> 
+       TacticAst.Note (loc, str)
+    ]
+  ];
+  
+  statement: [
+    [ ex = executable -> TacticAst.Executable (loc,ex)
+    | com = comment -> TacticAst.Comment (loc, com)
+    ]
+  ];
 END
 
 let exc_located_wrapper f =