diff options
| author | Hugo Herbelin | 2014-10-03 15:21:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-03 15:21:10 +0200 |
| commit | 9a82982c1eb8cb1d6a61d3d497d669591fb68747 (patch) | |
| tree | 946bacf9494795d8cfb34f633630bdab13feaa76 | |
| parent | 29844f673b5af1b0e50efc7b41cf5660d0a37d03 (diff) | |
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).
| -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 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 = diff --git a/test-suite/bugs/closed/3657.v b/test-suite/bugs/closed/3657.v new file mode 100644 index 0000000000..778fdab190 --- /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). |