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.
---
 pretyping/pretyping.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 122979c1a0..3b9a8e6a1d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -773,11 +773,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     in
     let app_f = 
       match EConstr.kind !evdref fj.uj_val with
-      | Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
+      | Const (p, u) when Recordops.is_primitive_projection p ->
+        let p = Option.get @@ Recordops.find_primitive_projection p in
 	let p = Projection.make p false in
-	let pb = Environ.lookup_projection p env.ExtraEnv.env in
-	let npars = pb.Declarations.proj_npars in
-	  fun n -> 
+        let npars = Projection.npars p in
+          fun n ->
 	    if n == npars + 1 then fun _ v -> mkProj (p, v)
 	    else fun f v -> applist (f, [v])
       | _ -> fun _ f v -> applist (f, [v])
@@ -905,6 +905,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let cloc = loc_of_glob_constr c in
 	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
     in
+    let ind = fst (fst (dest_ind_family indf)) in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
       user_err ?loc  (str "Destructing let is only for inductive types" ++
@@ -915,7 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
-      match get_projections env.ExtraEnv.env indf with
+      match Environ.get_projections env.ExtraEnv.env ind with
       | None ->
 	 List.map2 set_name (List.rev nal) cs.cs_args, false
       | Some ps ->
-- 
cgit v1.2.3