X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=634e8e291bcd2f38871290ac657f180588fd5e89;hb=d645b8bf30064e94ee9777d793854eebc921dfe0;hp=a539fef6c238783365912191b037985ec8a75a3d;hpb=a8fa717b6fe0f59ced6ac78f4d7bb6255a7405ec;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a539fef6c..634e8e291 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -245,9 +245,10 @@ EXTEND
     | "whd" -> `Whd ]
   ];
   tactic: [
-    [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
-    | [ IDENT "apply" | IDENT "Apply" ];
-      t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+    [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
+        return_tactic loc (TacticAst.Absurd t)
+    | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
+        return_tactic loc (TacticAst.Apply t)
     | [ IDENT "assumption" | IDENT "Assumption" ] ->
         return_tactic loc TacticAst.Assumption
     | [ IDENT "change" | IDENT "Change" ];
@@ -265,8 +266,7 @@ EXTEND
     | [ IDENT "discriminate" | IDENT "Discriminate" ];
       hyp = IDENT ->
         return_tactic loc (TacticAst.Discriminate hyp)
-    | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
-      t = tactic_term ->
+    | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
     | [ IDENT "elim" | IDENT "Elim" ];
       t1 = tactic_term;
@@ -369,6 +369,8 @@ EXTEND
         return_command loc (TacticAst.Undo (int_opt steps))
     | [ IDENT "redo"   | IDENT "Redo" ]; steps = OPT NUM ->
         return_command loc (TacticAst.Redo (int_opt steps))
+    | [ IDENT "check"   | IDENT "Check" ]; t = term ->
+        return_command loc (TacticAst.Check t)
     ]
   ];
 END