X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=50a373e49bf8b8389d0aad6836d2459c17f59a30;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=081055ce84d64ffea17c354bc635e4e091100775;hpb=396a578b680e7fdb9d262822184e52f0d4d5086b;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 081055ce8..50a373e49 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -170,8 +170,8 @@ EXTEND
 	let idents = match idents with None -> [] | Some idents -> idents in
 	GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "destruct"; t = tactic_term ->
-        GrafiteAst.Destruct (loc, t)
+    | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+        GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->
@@ -246,8 +246,6 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst" ->
-        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
@@ -639,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 ->