Add support so that the type of a match in an inductive type with let-in

is reduced as if without let-in, when applied to arguments.

This allows e.g. to have a head-betazeta-reduced goal in the following example.

Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
index e66bf922d..bb673f38c 100644
--- a/test-suite/bugs/closed/3210.v
+++ b/test-suite/bugs/closed/3210.v
@@ -7,3 +7,16 @@ Definition foo (x : Foo) : bool :=
   match x with
   I => true
   end.
+
+Definition foo' (x : Foo) : x = x.
+case x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+elim x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+induction x.
+match goal with |- I = I => idtac end. (* check form of the goal *)
+Undo 2.
+destruct x.
+match goal with |- I = I => idtac end. (* check form of the goal *)