Simplifying the declaration of constants bound to primitive projections.

We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.

We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.

We keep the unused code from inductiveops.ml for possible future use
though.

Include improvements contributed by Gaëtan Gilbert.

2 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
index e9c28faf1d..1dd89c9bcd 100644
--- a/test-suite/output/Projections.out
+++ b/test-suite/output/Projections.out
@@ -1,2 +1,17 @@
 fun S : store => S.(store_funcs)
      : store -> host_func
+a = 
+fun A : Type =>
+let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
+     : forall A : Type,
+       let B := A in
+       forall C : Type, U A C -> Type * Type * Type * (B * A * C)
+
+Arguments a (_ _)%type_scope
+b = 
+fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
+     : forall A : Type,
+       let B := A in
+       forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
+
+Arguments b (_ _)%type_scope
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 14d63d39c4..83a581338f 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -10,3 +10,12 @@ Section store.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
+
+Module LocalDefUnfolding.
+
+Unset Printing Projections.
+Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}.
+Print a.
+Print b.
+
+End LocalDefUnfolding.