From ad87baf78fb145517c4151c7a3f61d6b5e5fc550 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 7 Feb 2005 15:22:37 +0000 Subject: [PATCH] connected change tactic (proof of concept) --- helm/matita/matitaInterpreter.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.39.2