compose tactic restore and added nocomposites keyword

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index a0fd3335806f1468e3c637621b4cc4f9faef0c64..50a373e49bf8b8389d0aad6836d2459c17f59a30 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -637,11 +637,13 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; 
+      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
         let arity = match arity with None -> 0 | Some x -> x in
         let saturations = match saturations with None -> 0 | Some x -> x in
+        let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
-         (loc, UriManager.uri_of_string suri, true, arity, saturations)
+         (loc, UriManager.uri_of_string suri, composites, 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 ->