From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 checker/declarations.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'checker/declarations.ml')

diff --git a/checker/declarations.ml b/checker/declarations.ml
index a744a02279..0540227ccb 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -214,11 +214,7 @@ let rec map_kn f f' c =
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
       | Proj (p,t) -> 
-          let p' = 
-	    Projection.map (fun kn ->
-			    try fst (f' kn Univ.Instance.empty)
-			    with No_subst -> kn) p
-	  in
+          let p' = Projection.map f p in
 	  let t' = func t in
 	    if p' == p && t' == t then c
 	    else Proj (p', t')
@@ -495,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal eq_recarg
 
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (**********************************************************************)
 (* Representation of mutual inductive types in the kernel             *)
 (*
-- 
cgit v1.2.3