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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 31b881988..ececcf967 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 ->