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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 24cade68a..e84cd7084 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -556,8 +556,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 +566,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;