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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index d52b0e2de..31b881988 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -195,6 +195,10 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
+    | GrafiteAst.Compose (loc, t1, t2, 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)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->