diff options
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3657.v | 12 |
2 files changed, 16 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2ccad790f..3ee5e6afb 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 = diff --git a/test-suite/bugs/closed/3657.v b/test-suite/bugs/closed/3657.v new file mode 100644 index 000000000..778fdab19 --- /dev/null +++ b/test-suite/bugs/closed/3657.v @@ -0,0 +1,12 @@ +(* Check typing of replaced objects in change - even though the failure + was already a proper error message (but with a helpless content) *) + +Class foo {A} {a : A} := { bar := a; baz : bar = bar }. +Arguments bar {_} _ {_}. +Instance: forall A a, @foo A a. +intros; constructor. +abstract reflexivity. +Defined. +Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat. +Proof. + Fail change (bar (fun _ : Set => Set)) with (bar Set). |