From e7e9907596de471c2e9e5a3cf47b6d17b1af1892 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 11:44:24 +0000 Subject: [PATCH] Oooops. I forgot the convertibility test that makes the change tactic correct! --- helm/ocaml/tactics/primitiveTactics.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) 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 -- 2.39.2