X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=e2108381200b82ae16626d0a61fd11bafc419ac3;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=10a841e2eae14e01db81a03147ca3ace7ebb8bfe;hpb=3990759a81db3ce45bf4ec56e1985e532151f6e0;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 10a841e2e..e21083812 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -156,9 +156,10 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
-      specs = intros_spec ->
-        GrafiteAst.Compose (loc, t1, t2, specs)
+    | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
+      OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+        let times = match times with None -> 1 | Some i -> i in
+        GrafiteAst.Compose (loc, t1, t2, times, specs)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
@@ -290,11 +291,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: [
@@ -441,7 +459,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 ->