diff options
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12787.v | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index f1326a51a9..b4def7bb51 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1134,6 +1134,7 @@ let make_tuple env sigma (rterm,rty) lind = assert (not (noccurn sigma lind rty)); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in + let a = simpl env sigma a in let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in diff --git a/test-suite/bugs/closed/bug_12787.v b/test-suite/bugs/closed/bug_12787.v new file mode 100644 index 0000000000..2566e1f261 --- /dev/null +++ b/test-suite/bugs/closed/bug_12787.v @@ -0,0 +1,26 @@ +Inductive sigT3 {A: Type} {P: A -> Type} (Q: forall a: A, P a -> Type) := + existT3: forall a: A, forall b: P a, Q a b -> sigT3 Q +. + +Definition projT3_1 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) := + let 'existT3 _ x0 _ _ := a in x0. + +Definition projT3_2 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) : P (projT3_1 a) := + let 'existT3 _ x0 x1 _ := a in x1. + + + +Lemma projT3_3_eq' (A B: Type) (Q: B -> Type) (a b: sigT3 (fun (_: A) b => Q b)) (H: a = b) : + unit. +Proof. + destruct a as [x0 x1 x2], b as [y0 y1 y2]. + assert (H' := f_equal projT3_1 H). + cbn in H'. + subst x0. + assert (H' := f_equal (projT3_2 (P := fun _ => B)) H). + cbn in H'. + subst x1. + + injection H as H'. + exact tt. +Qed. |