Merge PR #7908: Projections use index representation

2 files changed, 16 insertions, 11 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index e425e6474d..614b2181d9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -73,7 +73,7 @@ let check_reference_arity ref =
 let check_arity = function
   | CL_FUN | CL_SORT -> ()
   | CL_CONST cst -> check_reference_arity (ConstRef cst)
-  | CL_PROJ cst -> check_reference_arity (ConstRef cst)
+  | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
   | CL_SECVAR id -> check_reference_arity (VarRef id)
   | CL_IND kn -> check_reference_arity (IndRef kn)
 
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
 
 let class_of_global = function
   | ConstRef sp -> 
-    if Environ.is_projection sp (Global.env ()) 
-    then CL_PROJ sp else CL_CONST sp
+    (match Recordops.find_primitive_projection sp with
+     | Some p -> CL_PROJ p | None -> CL_CONST sp)
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
     CL_FUN
   else
     match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
-    | CL_CONST p when Environ.is_projection p (Global.env ()) -> 
-      CL_PROJ p
+    | CL_CONST p when Recordops.is_primitive_projection p ->
+      CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
     | x -> x
       
 let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+  | CL_CONST sp -> Label.to_string (Constant.label sp)
+  | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
   | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
   | CL_SECVAR id -> Id.to_string id
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a8ce7d25a..6b5c538df2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -324,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 	  | Name fid -> try
 	    let kn, term = 
 	      if is_local_assum decl && primitive then
-		(** Already defined in the kernel silently *)
-                let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
-                let kn = destConstRef gr in
+                let p = Projection.Repr.make indsp
+                    ~proj_npars:mib.mind_nparams
+                    ~proj_arg:i
+                    (Label.of_id fid)
+                in
+                (** Already defined by declare_mind silently *)
+                let kn = Projection.Repr.constant p in
                 Declare.definition_message fid;
-                UnivNames.register_universe_binders gr ubinders;
-                kn, mkProj (Projection.make kn false,mkRel 1)
+                UnivNames.register_universe_binders (ConstRef kn) ubinders;
+                kn, mkProj (Projection.make p false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
 		let body = match decl with