diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-17 01:14:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-17 01:15:32 +0200 |
commit | beb3acd2fd3831404f0be2da61d3f28e210e8349 (patch) | |
tree | ac61acef6eef5ccf9c446b486c9443c915b83af1 | |
parent | 0147ae6ba6db24d4f9b29ff477d374a6abb103dd (diff) |
Add a test for bug #5321: clearbody breaks typing of goal.
The bug has been solved as a side-effect of the EConstr branch.
-rw-r--r-- | test-suite/bugs/closed/5321.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5321.v b/test-suite/bugs/closed/5321.v new file mode 100644 index 000000000..03514e23b --- /dev/null +++ b/test-suite/bugs/closed/5321.v @@ -0,0 +1,18 @@ +Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v) + : proj1_sig u = proj1_sig v + := f_equal (@proj1_sig _ _) p. + +Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v) + : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v + := match p with eq_refl => eq_refl end. + +Goal forall sz : nat, + let sz' := sz in + forall pf : sz = sz', + let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in + let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf -> +proj2_sig feq_refl = proj2_sig fpf. +Proof. + intros. + etransitivity; [ | exact (proj2_sig_path H) ]. + Fail clearbody fpf. |