From 730f21fb1b6329b9c16dd0021f5a8e2d573fcaae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Nov 2019 20:55:18 +0100
Subject: 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.
---
 test-suite/output/Projections.out | 15 +++++++++++++++
 test-suite/output/Projections.v   |  9 +++++++++
 2 files changed, 24 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3