From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 7 Feb 2005 15:22:37 +0000 (+0000)
Subject: connected change tactic (proof of concept)
X-Git-Tag: V_0_1_0~7
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad87baf78fb145517c4151c7a3f61d6b5e5fc550;hp=e54260c3938b4ec99e52ec7ca0297db6f7937cb1;p=helm.git

connected change tactic (proof of concept)
---

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 96145fa75..4d3137d55 100644
--- 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