X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=e6b3d8991493298421701895bdaf3332c20dd3fc;hb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;hp=cf2a6f95b6336e2f5581e6abd8d0f8b51e46d8c7;hpb=bb1b8417c52c48d5c58df54c82182d00d40cdf77;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index cf2a6f95b..e6b3d8991 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -180,6 +180,12 @@ EXTEND
     ]
   ];
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+  ntactic: [
+    [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+    | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
+        GrafiteAst.NChange (loc, what, with_what)
+    ]
+  ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->
         GrafiteAst.Absurd (loc, t)
@@ -227,12 +233,12 @@ EXTEND
         GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
-       (num, idents) = intros_spec ->
+       ispecs = intros_spec ->
         let pattern = match pattern with
            | None         -> None, [], Some Ast.UserInput
            | Some pattern -> pattern   
         in
-        GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
+        GrafiteAst.Elim (loc, what, using, pattern, ispecs)
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
         GrafiteAst.ElimType (loc, what, using, (num, idents))
@@ -462,6 +468,10 @@ EXTEND
       | IDENT "skip" -> GrafiteAst.Skip loc
       ]
     ];
+  ntheorem_flavour: [
+    [ [ IDENT "ntheorem"     ] -> `Theorem
+    ]
+  ];
   theorem_flavour: [
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
@@ -666,6 +676,9 @@ EXTEND
         GrafiteAst.Obj (loc, 
           Ast.Theorem 
             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
+    | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
@@ -698,8 +711,10 @@ EXTEND
         let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
          (loc, t, composites, arity, saturations)
-    | IDENT "unification"; IDENT "hint"; t = tactic_term ->
-        GrafiteAst.UnificationHint (loc, t)
+    | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
+        GrafiteAst.PreferCoercion (loc, t)
+    | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+        GrafiteAst.UnificationHint (loc, t, n)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
@@ -729,6 +744,8 @@ EXTEND
     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
         GrafiteAst.Tactic (loc, Some tac, punct)
     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+    | tac = ntactic; punct = punctuation_tactical ->
+        GrafiteAst.NTactic (loc, tac, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)