fixed Whelp stuff

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9b0617bc8010482decadcd1c31363ea5f7c9d3b8..5e70ff571ecd62b8a3402da395c8aebee9b5312a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -485,9 +485,15 @@ EXTEND
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
-        TacticAst.Match (loc,t)
+        TacticAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
-        TacticAst.Instance (loc,t)
+        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)
   ]];