X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=b3bbaf3f8d94d68d3a6cfe6c8b4b90597273f744;hb=9c2f282765ec75a3c9aafc9e73e6626588891abe;hp=44dec6d32bf6adfc4aef459977bb26c861fe26cb;hpb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 44dec6d32..b3bbaf3f8 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -180,6 +180,15 @@ 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)
+    | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NElim (loc, what, where)
+    | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+    ]
+  ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->
         GrafiteAst.Absurd (loc, t)
@@ -462,6 +471,10 @@ EXTEND
       | IDENT "skip" -> GrafiteAst.Skip loc
       ]
     ];
+  ntheorem_flavour: [
+    [ [ IDENT "ntheorem"     ] -> `Theorem
+    ]
+  ];
   theorem_flavour: [
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
@@ -666,6 +679,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))
@@ -700,8 +716,8 @@ EXTEND
          (loc, t, composites, arity, saturations)
     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
         GrafiteAst.PreferCoercion (loc, t)
-    | IDENT "unification"; IDENT "hint"; t = tactic_term ->
-        GrafiteAst.UnificationHint (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 ->
@@ -731,6 +747,10 @@ 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)
+    | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
+        GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)