1 files changed, 54 insertions, 18 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d070edea..aedef40e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -44,7 +44,7 @@ type struc_typ = {
 let structure_table =
   Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
 let projection_table =
-  Summary.ref Cmap.empty ~name:"record-projs"
+  Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
 
 (* TODO: could be unify struc_typ and struc_tuple ? in particular,
    is the inductive always (fst constructor) ? It seems so... *)
@@ -53,7 +53,9 @@ type struc_tuple =
     inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 let load_structure i (_,(ind,id,kl,projs)) =
-  let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let open Declarations in
+  let mib, mip = Global.lookup_inductive ind in
+  let n = mib.mind_nparams in
   let struc =
     { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
@@ -69,8 +71,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
-   List.smartmap
-     (Option.smartmap (fun kn -> fst (subst_con_kn subst kn)))
+   List.Smart.map
+     (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
     projs
   in
   let id' = fst (subst_constructor subst id) in
@@ -107,6 +109,34 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
+let prim_table =
+  Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
+
+let load_prim i (_,p) =
+  prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table
+
+let cache_prim p = load_prim 1 p
+
+let subst_prim (subst,p) = subst_proj_repr subst p
+
+let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p)
+
+let inPrim : Projection.Repr.t -> obj =
+  declare_object {
+    (default_object "PRIMPROJS") with
+    cache_function = cache_prim ;
+    load_function = load_prim;
+    subst_function = subst_prim;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_prim }
+
+let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p)
+
+let is_primitive_projection c = Cmap_env.mem c !prim_table
+
+let find_primitive_projection c =
+  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
@@ -144,13 +174,13 @@ type obj_typ = {
   o_TCOMPS : constr list } (* ordered *)
 
 type cs_pattern =
-    Const_cs of global_reference
+    Const_cs of GlobRef.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
 
 let eq_cs_pattern p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2
+| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2
 | Prod_cs, Prod_cs -> true
 | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
 | Default_cs, Default_cs -> true
@@ -199,7 +229,7 @@ let warn_projection_no_head_constant =
           let env = Termops.push_rels_assum sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-          let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
+          let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
           ++ term_pp ++ strbrk " in canonical instance "
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
@@ -211,7 +241,7 @@ let compute_canonical_projections warn (con,ind) =
   let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
   let c = Environ.constant_value_in env (con,u) in
-  let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+  let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
   let lt = List.rev_map snd sign in
@@ -265,8 +295,12 @@ let add_canonical_structure warn o =
       in match ocs with
         | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
-              let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
-              and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
+              (* XXX: Undesired global access to env *)
+              let env = Global.env () in
+              let sigma = Evd.from_env env in
+              let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
+              and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
+              in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
               if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
@@ -304,36 +338,38 @@ let error_not_structure ref description =
   user_err ~hdr:"object_declare"
     (str"Could not declare a canonical structure " ++
        (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
-          str(description)))
+          description))
 
 let check_and_decompose_canonical_structure ref =
   let sp =
     match ref with
       ConstRef sp -> sp
-    |  _ -> error_not_structure ref "Expected an instance of a record or structure."
+    |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
   in
   let env = Global.env () in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
-    | None -> error_not_structure ref "Could not find its value in the global environment." in
-  let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+    | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
     | App (f,args) -> f,args
     | _ ->
-       error_not_structure ref "Expected a record or structure constructor applied to arguments." in
+       error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in
   let indsp = match kind f with
     | Construct ((indsp,1),u) -> indsp
-    | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+    | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
   let s =
     try lookup_structure indsp
     with Not_found ->
       error_not_structure ref
-        ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
+        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
-    error_not_structure ref "Got too few arguments to the record or structure constructor.";
+    error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
 
 let declare_canonical_structure ref =