connected change tactic (proof of concept)

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 96145fa7505ea27a09bdea694b0914fd49856be8..4d3137d55e74e56bea5de9e36979a7993b2a2e74 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -556,10 +556,14 @@ class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
           Tactics.replace ~what:(self#disambiguate what)
             ~with_what:(self#disambiguate with_what)
       | TacticAst.Auto -> Tactics.auto_new ~dbd
+      | TacticAst.Change (what, with_what, _) ->
+          let what = self#disambiguate what in
+          let with_what = self#disambiguate with_what in
+          Tactics.change ~what ~with_what
     (*
       (* TODO Zack a lot more of tactics to be implemented here ... *)
-      | TacticAst.Change of 'term * 'term * 'ident option
       | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+      | TacticAst.Change of 'term * 'term * 'ident option
       | TacticAst.Decompose of 'ident * 'ident list
       | TacticAst.Discriminate of 'ident
       | TacticAst.Fold of reduction_kind * 'term