X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=431b15ae83d807617aeef459fbec3d9e621ac068;hb=3b4ce4f34c41a0a588cbb02e69a728d296b75359;hp=9b0617bc8010482decadcd1c31363ea5f7c9d3b8;hpb=63b1ff9601a54dba2bed63c2b58ec909dc162471;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9b0617bc8..431b15ae8 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -250,8 +250,6 @@ EXTEND
         b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
-      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "logic_add" LEFTA   [ (* nothing here by default *) ]
     | "logic_mult" LEFTA  [ (* nothing here by default *) ]
@@ -277,6 +275,8 @@ EXTEND
         b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
+      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
@@ -391,7 +391,7 @@ EXTEND
         (match (pat, terms) with
         | None, [] -> TacticAst.Reduce (loc, kind, None)
         | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
-        | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+        | Some pat, [] -> fail loc "Missing term [list]"
         | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
     | [ IDENT "reflexivity" ] ->
         TacticAst.Reflexivity loc
@@ -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)
   ]];