From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 11:44:24 +0000 (+0000)
Subject: Oooops. I forgot the convertibility test that makes the change tactic correct!
X-Git-Tag: PRE_GETTER_STORAGE~96
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7e9907596de471c2e9e5a3cf47b6d17b1af1892;p=helm.git

Oooops. I forgot the convertibility test that makes the change tactic correct!
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 606ae89d0..8766a044a 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -632,9 +632,16 @@ let change_tac ~pattern with_what  =
             CicSubstitution.lift (context_of_t_len - context'_len)
              with_what_in_context'
            else
-            with_what
-          in
-           t, with_what_in_context_of_t) terms)
+            with_what in
+          let _,u =
+           CicTypeChecker.type_of_aux' metasenv context_of_t with_what
+            CicUniv.empty_ugraph in
+          let b,_ =
+           CicReduction.are_convertible ~metasenv context_of_t t with_what u in
+          if b then
+           t, with_what_in_context_of_t
+          else
+           raise NotConvertible) terms)
     in
      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
       ~where:where in