]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_parser/grafiteParser.ml
Coercions are now generalized to the general form
[helm.git] / components / grafite_parser / grafiteParser.ml
index e2108381200b82ae16626d0a61fd11bafc419ac3..081055ce84d64ffea17c354bc635e4e091100775 100644 (file)
@@ -639,9 +639,11 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
         let arity = match arity with None -> 0 | Some x -> x in
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+        let saturations = match saturations with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion
+         (loc, UriManager.uri_of_string suri, true, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->