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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 24cade68a..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 ->
@@ -556,8 +559,9 @@ EXTEND
       paramspec = OPT inverter_param_list ; 
       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
         G.NInverter (loc,name,indty,paramspec,outsort)
-    | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
+    | IDENT "universe"; cyclic = OPT [ IDENT "cyclic" -> () ] ; IDENT "constraint"; u1 = tactic_term; 
         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+        let acyclic = match cyclic with None -> true | Some () -> false in
         let urify = function 
           | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
@@ -565,7 +569,7 @@ EXTEND
         in
         let u1 = urify u1 in
         let u2 = urify u2 in
-         G.NUnivConstraint (loc,u1,u2)
+         G.NUnivConstraint (loc,acyclic,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
     | IDENT "coercion"; name = IDENT;