removed duplicate entry

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 2863d5374a4657be619fae7d0ccf670c1130f7ad..f8840cd77a730cf96b1bdf085b6d3b49c3869fd9 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -67,10 +67,9 @@ EXTEND
    [ hyp_paths =
       LIST0
        [ id = IDENT ;
-         path = OPT [SYMBOL ":" ; path = term -> path ] ->
-         (id,match path with Some p -> p | None -> Ast.UserInput) ]
-       SEP SYMBOL ";";
-     goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
+         path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
+         (id,match path with Some p -> p | None -> Ast.UserInput) ];
+     goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
       let goal_path =
        match goal_path, hyp_paths with
           None, [] -> Ast.UserInput
@@ -84,7 +83,7 @@ EXTEND
     [ res = OPT [
        "in";
        wanted_and_sps =
-        [ "match" ; wanted = term ;
+        [ "match" ; wanted = tactic_term ;
           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
            Some wanted,sps
         | sps = sequent_pattern_spec ->
@@ -318,7 +317,6 @@ EXTEND
   macro: [
     [ [ IDENT "quit"  ] -> GrafiteAst.Quit loc
 (*     | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-    | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
 (*     | [ IDENT "undo"   ]; steps = OPT NUMBER ->
         GrafiteAst.Undo (loc, int_opt steps)
     | [ IDENT "redo"   ]; steps = OPT NUMBER ->