new compose tactic, still undocumented.

[helm.git] / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index d52b0e2de830105c80ee5837fe5902e583b2edc4..31b881988076b4c46a72adbbb0ee9a64fc798c9b 100644 (file)
--- 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 ->