X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=c1b347071b799ce5ed9630f32ffc15672cd72b15;hb=b6ceb877c05d27705ef163488aee38e60a86886c;hp=e84cd708495bf436cd79853ee5f8fa242b059c9d;hpb=d51f9674886d1e609a6ea792b65871dcde4f6503;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index e84cd7084..c1b347071 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-(* $Id$ *)
+(* $Id: grafiteParser.ml 13176 2016-04-18 15:29:33Z fguidi $ *)
 
 module N  = NotationPt
 module G  = GrafiteAst
@@ -239,6 +239,7 @@ EXTEND
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
+    | IDENT "assume"; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
     ]
   ];
   auto_fixed_param: [
@@ -526,7 +527,9 @@ EXTEND
         G.NObj (loc, 
           N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
           true)
-    | src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
+    | src = source; IDENT "axiom"; i = index; name = IDENT;
+        params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term -> (* FG: params added *)
+        let typ = shift_params `Forall params typ in
         let attrs = src, `Axiom, `Regular in
 	G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
     | src = source; IDENT "inductive"; spec = inductive_spec ->