From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Jun 2005 17:09:16 +0000 (+0000)
Subject: replace generalized to patterns
X-Git-Tag: INDEXING_NO_PROOFS~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27299607c6c7329e783f72d92c5da1796d41a5d6;p=helm.git

replace generalized to patterns
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 37c96ce4e..a60e9e20d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -25,7 +25,8 @@ let tactic_of_ast = function
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Auto (_,depth,width) -> 
       AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
-  | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
+  | TacticAst.Change (_, what, with_what, pattern) ->
+     Tactics.change ~what ~with_what ~pattern
   | TacticAst.Clear (_,id) -> Tactics.clear id
   | TacticAst.ClearBody (_,id) -> Tactics.clearbody id
   | TacticAst.Contradiction _ -> Tactics.contradiction