X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=cf2f7b1fce827425e78c96322a55c057a22d878e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2863d5374a4657be619fae7d0ccf670c1130f7ad;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 2863d5374..cf2f7b1fc 100644
--- 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 ->
@@ -448,10 +446,10 @@ EXTEND
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
-    | flavour = theorem_flavour; name = IDENT;
-      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+    | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+      body = term ->
         GrafiteAst.Obj (loc,
-          GrafiteAst.Theorem (flavour, name, Ast.Implicit, body))
+          GrafiteAst.Theorem (flavour, name, Ast.Implicit, Some body))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
@@ -464,10 +462,10 @@ EXTEND
           let body = Ast.Ident (name,None) in
           GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty,
             Some (Ast.LetRec (ind_kind, defs, body))))
-    | [ IDENT "inductive" ]; spec = inductive_spec ->
+    | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
-    | [ IDENT "coinductive" ]; spec = inductive_spec ->
+    | IDENT "coinductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
@@ -492,7 +490,7 @@ EXTEND
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
-    | IDENT "metadata"; [IDENT "dependency" | IDENT "baseuri" ] ; URI ->
+    | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI ->
         (** metadata commands lives only in .moo, where they are in marshalled
          * form *)
         raise (CicNotationParser.Parse_error (loc, "metadata not allowed here"))