Fixing #3657 (check that both sides of a "change with" have the same

type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).

1 files changed, 4 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2ccad790f1..3ee5e6afbc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -467,9 +467,11 @@ type change_arg = env -> evar_map -> evar_map * constr
 (* Now we introduce different instances of the previous tacticals *)
 let change_and_check cv_pb t env sigma c =
   let sigma, t' = t env sigma in
+  let sigma, b = infer_conv ~pb:cv_pb env sigma (Retyping.get_type_of env sigma t') (Retyping.get_type_of env sigma c) in
+  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-    if b then sigma, t'
-    else errorlabstrm "convert-check-hyp" (str "Not convertible.")
+  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+  sigma, t'
 
 let change_and_check_subst cv_pb subst t env sigma c =
   let t' env sigma =