X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=d4ab241cbbc64cfe8638980b81e4e051dcf9e57f;hb=361e74e8f714a12b22730fe3a303b12b10d4d7b6;hp=31b881988076b4c46a72adbbb0ee9a64fc798c9b;hpb=936f80cf031a7b034dd70fef49abb90e69f2e680;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 31b881988..d4ab241cb 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -195,10 +195,16 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
-    | GrafiteAst.Compose (loc, t1, t2, spec) ->
+    | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
         let metasenv,t1 = disambiguate_term context metasenv t1 in
-        let metasenv,t2 = disambiguate_term context metasenv t2 in
-        metasenv,   GrafiteAst.Compose (loc, t1, t2, spec)
+        let metasenv,t2 = 
+          match t2 with
+          | None -> metasenv, None
+          | Some t2 -> 
+              let m, t2 = disambiguate_term context metasenv t2 in
+              m, Some t2
+        in
+        metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
@@ -391,7 +397,8 @@ let rec disambiguate_tactic
 	    `Auto _ as t -> metasenv,t
 	  | `Term t -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
-	      metasenv,`Term t in
+	      metasenv,`Term t
+          | `Proof as t -> metasenv,t in
 	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)