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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 45a71f174..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 ->
@@ -291,11 +289,28 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 	 GrafiteAst.Case(loc,id,params)
-    | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params  ] ; cont=rewriting_step_continuation ->
-     GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
-    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
-      cont=rewriting_step_continuation  ->
-     GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+    | start =
+       [ IDENT "conclude" -> None
+       | IDENT "obtain" ; name = IDENT -> Some name ] ;
+      termine = tactic_term ;
+      SYMBOL "=" ;
+      t1=tactic_term ;
+      IDENT "by" ;
+      t2 =
+       [ t=tactic_term -> `Term t
+       | SYMBOL "_" ; params = auto_params' -> `Auto params
+       | IDENT "proof" -> `Proof] ;
+      cont = rewriting_step_continuation ->
+       GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+    | SYMBOL "=" ;
+      t1=tactic_term ;
+      IDENT "by" ;
+      t2=
+       [ t=tactic_term -> `Term t
+       | SYMBOL "_" ; params = auto_params' -> `Auto params
+       | IDENT "proof" -> `Proof] ;
+      cont=rewriting_step_continuation ->
+       GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
 ];
   auto_params: [
@@ -442,7 +457,8 @@ EXTEND
 	 in
 	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
 	 GrafiteAst.Inline (loc,style,suri,prefix)
-    | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
+         if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term -> 
@@ -621,9 +637,13 @@ 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; composites = OPT (IDENT "nocomposites") ->
         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
+        let composites = match composites with None -> true | Some _ -> false in
+        GrafiteAst.Coercion
+         (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 ->