changed match syntax:

[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 9f5fd193e9d170c05ef4fe9473e175c9805d251d..78d1bf181c8b99c1d14b965244eac25eacc7ebc0 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -279,6 +279,7 @@ EXTEND
       | n = substituted_name -> return_term loc n
       | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
       | IMPLICIT -> return_term loc CicAst.Implicit
+      | PLACEHOLDER -> return_term loc CicAst.UserInput
       | m = META;
         substs = [
           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
@@ -293,7 +294,7 @@ EXTEND
             return_term loc (CicAst.Meta (index, substs))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+        indty_ident = OPT ["in" ; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -322,7 +323,8 @@ EXTEND
   reduction_kind: [
     [ [ IDENT "reduce" ] -> `Reduce
     | [ IDENT "simplify" ] -> `Simpl
-    | [ IDENT "whd" ] -> `Whd ]
+    | [ IDENT "whd" ] -> `Whd 
+    | [ IDENT "normalize" ] -> `Normalize ]
   ];
   tactic: [
     [ [ IDENT "absurd" ]; t = tactic_term ->
@@ -373,7 +375,7 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         TacticAst.Intros (loc, num, idents)
     | [ IDENT "intro" ] ->
-        TacticAst.Intros (loc, None, [])
+        TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
@@ -389,6 +391,8 @@ EXTEND
         | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
         | Some pat, [] -> fail loc "Missing term [list]"
         | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+    | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+        TacticAst.ReduceAt (loc, kind, where, pat)
     | [ IDENT "reflexivity" ] ->
         TacticAst.Reflexivity loc
     | [ IDENT "replace" ];
@@ -469,14 +473,14 @@ EXTEND
       (params, ind_types)
   ] ];
 
-  macro: [[
-      [ IDENT "abort" ] -> TacticAst.Abort loc
-    | [ IDENT "quit"  ] -> TacticAst.Quit loc
+  macro: [
+    [ [ IDENT "quit"  ] -> TacticAst.Quit loc
+(*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-    | [ IDENT "undo"   ]; steps = OPT NUM ->
+(*     | [ IDENT "undo"   ]; steps = OPT NUM ->
         TacticAst.Undo (loc, int_opt steps)
     | [ IDENT "redo"   ]; steps = OPT NUM ->
-        TacticAst.Redo (loc, int_opt steps)
+        TacticAst.Redo (loc, int_opt steps) *)
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
@@ -491,7 +495,8 @@ EXTEND
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-  ]];
+    ]
+  ];
 
   alias_spec: [
     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->