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 606ae89d0768ff4e74ae953b2d55906e06ab2554..8766a044a576ead6f30826bc899dcd28b1999b72 100644 (file)
--- 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