[recordops] complete API rewrite; the module is now called [structures]

26 files changed, 503 insertions, 372 deletions

diff --git a/dev/base_include b/dev/base_include
index 061bf1f3e1..b761924b46 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -68,7 +68,7 @@ open Constr_matching
 open Glob_term
 open Glob_ops
 open Coercion
-open Recordops
+open Structures
 open Detyping
 open Reductionops
 open Evarconv
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3cabf52197..f687c4a640 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -27,6 +27,7 @@ open Glob_term
 open Glob_ops
 open Pattern
 open Detyping
+open Structures
 
 module NamedDecl = Context.Named.Declaration
 (*i*)
@@ -232,7 +233,7 @@ let get_record_print =
 
 let is_record indsp =
   try
-    let _ = Recordops.lookup_structure indsp in
+    let _ = Structure.find indsp in
     true
   with Not_found -> false
 
@@ -407,7 +408,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
 let extern_record_pattern cstrsp args =
   try
     if !Flags.raw_print then raise Exit;
-    let projs = Recordops.lookup_projections (fst cstrsp) in
+    let projs = Structure.find_projections (fst cstrsp) in
     if PrintingRecord.active (fst cstrsp) then
       ()
     else if PrintingConstructor.active (fst cstrsp) then
@@ -614,9 +615,12 @@ let is_gvar id c = match DAst.get c with
 let is_projection nargs r =
   if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then
     try
-      let n = Recordops.find_projection_nparams r + 1 in
-      if n <= nargs then Some n
-      else None
+      match r with
+      | GlobRef.ConstRef c ->
+        let n = Structure.projection_nparams c + 1 in
+        if n <= nargs then Some n
+        else None
+      | _ -> None
     with Not_found -> None
   else None
 
@@ -689,33 +693,29 @@ let extern_record ref args =
   try
     if !Flags.raw_print then raise Exit;
     let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
-    let struc = Recordops.lookup_structure (fst cstrsp) in
+    let struc = Structure.find (fst cstrsp) in
     if PrintingRecord.active (fst cstrsp) then
       ()
     else if PrintingConstructor.active (fst cstrsp) then
       raise Exit
     else if not (get_record_print ()) then
       raise Exit;
-    let projs = struc.Recordops.s_PROJ in
-    let locals = struc.Recordops.s_PROJKIND in
+    let projs = struc.Structure.projections in
     let rec cut args n =
       if Int.equal n 0 then args
       else
         match args with
         | [] -> raise No_match
         | _ :: t -> cut t (n - 1) in
-    let args = cut args struc.Recordops.s_EXPECTEDPARAM in
-    let rec ip projs locs args acc =
+    let args = cut args struc.Structure.nparams in
+    let rec ip projs args acc =
       match projs with
       | [] -> acc
-      | None :: q -> raise No_match
-      | Some c :: q ->
-         match locs with
-         | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-         | { Recordops.pk_true_proj = false } :: locs' ->
+      | { Structure.proj_body = None } :: _ -> raise No_match
+      | { Structure.proj_body = Some c; proj_true = false } :: q ->
             (* we don't want to print locals *)
-            ip q locs' args acc
-         | { Recordops.pk_true_proj = true } :: locs' ->
+            ip q args acc
+      | { Structure.proj_body = Some c; proj_true = true } :: q ->
             match args with
             | [] -> raise No_match
             (* we give up since the constructor is not complete *)
@@ -723,9 +723,9 @@ let extern_record ref args =
                let arg = Lazy.force arg in
                let loc = arg.CAst.loc in
                let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in
-               ip q locs' tail ((ref, arg) :: acc)
+               ip q tail ((ref, arg) :: acc)
     in
-    Some (List.rev (ip projs locals args []))
+    Some (List.rev (ip projs args []))
   with
     | Not_found | No_match | Exit -> None
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7c63ebda3a..958e1408f8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -24,6 +24,7 @@ open Glob_term
 open Glob_ops
 open Patternops
 open Pretyping
+open Structures
 open Cases
 open Constrexpr
 open Constrexpr_ops
@@ -34,6 +35,7 @@ open Inductiveops
 open Context.Rel.Declaration
 open NumTok
 
+
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
     - it replaces notations by their value (scopes stuff are here)
@@ -100,7 +102,7 @@ type internalization_error =
   | NonLinearPattern of Id.t
   | BadPatternsNumber of int * int
   | NotAProjection of qualid
-  | ProjectionsOfDifferentRecords of Recordops.struc_typ * Recordops.struc_typ
+  | ProjectionsOfDifferentRecords of Structure.t * Structure.t
 
 exception InternalizationError of internalization_error
 
@@ -126,8 +128,8 @@ let explain_bad_patterns_number n1 n2 =
   str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
   str " but found " ++ int n2
 
-let inductive_of_record record =
-  let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+let inductive_of_record s =
+  let inductive = GlobRef.IndRef (s.Structure.name) in
   Nametab.shortest_qualid_of_global Id.Set.empty inductive
 
 let explain_field_not_a_projection field_id =
@@ -1130,8 +1132,10 @@ let intern_reference qid =
 
 let intern_projection qid =
   try
-    let gr = Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) in
-    (gr, Recordops.find_projection gr)
+    match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with
+    | GlobRef.ConstRef c as gr ->
+        (gr, Structure.find_from_projection c)
+    | _ -> raise Not_found
   with Not_found ->
     Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
 
@@ -1296,8 +1300,8 @@ let check_applied_projection isproj realref qid =
     let is_prim = match realref with
       | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false
       | Some (ConstRef c) ->
-        if Recordops.is_primitive_projection c then true
-        else if Recordops.is_projection c then false
+        if PrimitiveProjections.mem c then true
+        else if Structure.is_projection c then false
         else error_nonprojection_syntax ?loc:qid.loc qid
         (* TODO check projargs, note we will need implicit argument info *)
     in
@@ -1498,18 +1502,18 @@ let sort_fields ~complete loc fields completer =
     | (first_field_ref, _):: _ ->
         let (first_field_glob_ref, record) = intern_projection first_field_ref in
         (* the number of parameters *)
-        let nparams = record.Recordops.s_EXPECTEDPARAM in
+        let nparams = record.Structure.nparams in
         (* the reference constructor of the record *)
-        let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in
+        let base_constructor = GlobRef.ConstructRef (record.Structure.name,1) in
         let () = check_duplicate ?loc fields in
-        let build_proj idx proj kind =
-          if proj = None && complete then
+        let build_proj idx proj =
+          if proj.Structure.proj_body = None && complete then
             (* we don't want anonymous fields *)
             user_err ?loc (str "This record contains anonymous fields.")
           else
-            (idx, proj, kind.Recordops.pk_true_proj) in
+            (idx, proj.Structure.proj_body, proj.Structure.proj_true) in
         let proj_list =
-          List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in
+          List.map_i build_proj 1 record.Structure.projections in
         (* now we want to have all fields assignments indexed by their place in
            the constructor *)
         let rec index_fields fields remaining_projs acc =
@@ -1538,7 +1542,7 @@ let sort_fields ~complete loc fields completer =
                      (* For terms, we keep only regular fields *)
                      None
                    else
-                     Some (idx, completer idx field_ref record.Recordops.s_CONST) in
+                     Some (idx, completer idx field_ref (record.Structure.name,1)) in
                  List.map_filter complete_field remaining_projs in
                List.rev_append remaining_fields acc
         in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c5ac57a2cd..d2fb773dc4 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -291,6 +291,11 @@ let subst_ind sub (ind,i as indi) =
   let ind' = subst_mind sub ind in
     if ind' == ind then indi else ind',i
 
+let subst_constructor subst (ind,j as ref) =
+  let ind' = subst_ind subst ind in
+  if ind==ind' then ref
+  else (ind',j)
+
 let subst_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 9cf270cff7..e7bfceb4de 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -127,6 +127,9 @@ val subst_mind :
 val subst_ind :
   substitution -> inductive -> inductive
 
+val subst_constructor :
+  substitution -> constructor -> constructor
+
 val subst_pind : substitution -> pinductive -> pinductive
 
 val subst_kn :
diff --git a/library/globnames.ml b/library/globnames.ml
index 654349dea0..491c89e68e 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,10 +31,6 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
-let subst_constructor subst (ind,j as ref) =
-  let ind' = subst_ind subst ind in
-  if ind==ind' then ref
-  else (ind',j)
 
 let subst_global_reference subst ref = match ref with
   | VarRef var -> ref
diff --git a/library/globnames.mli b/library/globnames.mli
index 8acea5ef28..58e0efbc7a 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -34,7 +34,6 @@ val destConstructRef : GlobRef.t -> constructor
 val is_global : GlobRef.t -> constr -> bool
 [@@ocaml.deprecated "Use [Constr.isRefX] instead."]
 
-val subst_constructor : substitution -> constructor -> constructor
 val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0cad192332..ca4f5429a2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -22,7 +22,6 @@ open Reductionops
 open Inductive
 open Termops
 open Inductiveops
-open Recordops
 open Namegen
 open Miniml
 open Table
@@ -531,7 +530,7 @@ and extract_really_ind env kn mib =
           let n = nb_default_params env sg (EConstr.of_constr ty) in
           let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
           in
-          List.iter (Option.iter check_proj) (lookup_projections ip)
+          List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip)
         with Not_found -> ()
         end;
         Record field_glob
@@ -1129,7 +1128,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
           | Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
           | Def c ->
-             (match Recordops.find_primitive_projection kn with
+             (match Structures.PrimitiveProjections.find_opt kn with
               | None -> mk_typ (get_body c)
               | Some p ->
                 let body = fake_match_projection env p in
@@ -1142,7 +1141,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
           | Primitive _ | Undef _ -> warn_info (); mk_ax ()
           | Def c ->
-             (match Recordops.find_primitive_projection kn with
+             (match Structures.PrimitiveProjections.find_opt kn with
               | None -> mk_def (get_body c)
               | Some p ->
                 let body = fake_match_projection env p in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7774258fca..805be1fc87 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -22,7 +22,6 @@ open Vars
 open Libnames
 open Tactics
 open Termops
-open Recordops
 open Tacmach
 open Glob_term
 open Util
@@ -333,7 +332,8 @@ type tpattern = {
 let all_ok _ _ = true
 
 let proj_nparams c =
-  try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0
+  try 1 + Structures.Structure.projection_nparams c
+  with Not_found -> 0
 
 let isRigid c = match kind c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
@@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u =
   | _ -> KpatRigid in
   sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t}
 
-let nb_cs_proj_args pc f u =
+let nb_cs_proj_args ise pc f u =
+  let open Structures in
+  let open ValuePattern in
   let na k =
-    List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
+    let open CanonicalSolution in
+    let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in
+    List.length cvalue_arguments in
   let nargs_of_proj t = match kind t with
       | App(_,args) -> Array.length args
       | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
@@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u =
   | Prod _ -> na Prod_cs
   | Sort s -> na (Sort_cs (Sorts.family s))
   | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f
-  | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
+  | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f
   | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f))
   | _ -> -1
   with Not_found -> -1
@@ -467,7 +471,7 @@ let splay_app ise =
   | Cast _ | Evar _ -> loop c [| |]
   | _ -> c, [| |]
 
-let filter_upat i0 f n u fpats =
+let filter_upat ise i0 f n u fpats =
   let na = Array.length u.up_a in
   if n < na then fpats else
   let np = match u.up_k with
@@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats =
   | KpatRigid when isRigid f -> na
   | KpatFlex -> na
   | KpatProj pc ->
-    let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np
+    let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np
   | _ -> -1 in
   if np < na then fpats else
   let () = if !i0 < np then i0 := n in (u, np) :: fpats
@@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
  let failed_because_of_TC = ref false in
  let rec aux upats env sigma0 ise c =
   let f, a = splay_app ise c in let i0 = ref (-1) in
-  let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
+  let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in
   while !i0 >= 0 do
     let i = !i0 in i0 := -1;
     let one_match (u, np) =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e1d6fff3e4..285fea183b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,7 +19,7 @@ open Context
 open Vars
 open Reduction
 open Reductionops
-open Recordops
+open Structures
 open Evarutil
 open Evardefine
 open Evarsolve
@@ -230,33 +230,30 @@ let occur_rigidly flags env evd (evk,_) t =
    projection would have been reduced) *)
 
 let check_conv_record env sigma (t1,sk1) (t2,sk2) =
+  let open ValuePattern in
   let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
-  let canon_s,sk2_effective =
+  let (sigma, solution), sk2_effective =
     try
       match EConstr.kind sigma t2 with
         Prod (_,a,b) -> (* assert (l2=[]); *)
           let _, a, b = destProd sigma t2 in
           if noccurn sigma 1 b then
-            lookup_canonical_conversion env (proji, Prod_cs),
+            CanonicalSolution.find env sigma (proji, Prod_cs),
             (Stack.append_app [|a;pop b|] Stack.empty)
           else raise Not_found
       | Sort s ->
         let s = ESorts.kind sigma s in
-        lookup_canonical_conversion env
+        CanonicalSolution.find env sigma
           (proji, Sort_cs (Sorts.family s)),[]
       | Proj (p, c) ->
-        lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2
+        CanonicalSolution.find env sigma(proji, Proj_cs (Names.Projection.repr p)), Stack.append_app [|c|] sk2
       | _ ->
         let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
-          lookup_canonical_conversion env (proji, Const_cs c2),sk2
+          CanonicalSolution.find env sigma (proji, Const_cs c2),sk2
     with Not_found ->
-      let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in
-        (c,cs),[]
+      CanonicalSolution.find env sigma (proji,Default_cs), []
   in
-  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
-        o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
-  let us = List.map EConstr.of_constr us in
-  let params = List.map EConstr.of_constr params in
+  let open CanonicalSolution in
   let params1, c1, extra_args1 =
     match arg with
     | Some c -> (* A primitive projection applied to c *)
@@ -267,28 +264,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
         with _ -> raise Not_found
       in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
-      match Stack.strip_n_app nparams sk1 with
+      match Stack.strip_n_app solution.nparams sk1 with
       | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
       | _ -> raise Not_found in
   let us2,extra_args2 =
-    let l_us = List.length us in
+    let l_us = List.length solution.cvalue_arguments in
       if Int.equal l_us 0 then Stack.empty,sk2_effective
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let u, ctx' = UnivGen.fresh_instance_from ctx None in
-  let subst = Univ.make_inverse_instance_subst u in
-  let c = EConstr.of_constr c in
-  let c' = subst_univs_level_constr subst c in
-  let t' = EConstr.of_constr t' in
-  let t' = subst_univs_level_constr subst t' in
-  let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
-  let params = List.map (fun c -> subst_univs_level_constr subst c) params in
-  let us = List.map (fun c -> subst_univs_level_constr subst c) us in
-  let h, _ = decompose_app_vect sigma t' in
-    ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
-    (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
-    (n, Stack.zip sigma (t2,sk2))
+  let h, _ = decompose_app_vect sigma solution.body in
+    sigma,(h, t2),solution.constant,solution.abstractions_ty,(Stack.append_app_list solution.params Stack.empty,params1),
+    (Stack.append_app_list solution.cvalue_arguments Stack.empty,us2),(extra_args1,extra_args2),c1,
+    (solution.cvalue_abstraction, Stack.zip sigma (t2,sk2))
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
@@ -926,7 +914,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         and f2 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i
+             else conv_record flags env
                (try check_conv_record env i appr1 appr2
                 with Not_found -> check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
@@ -989,7 +977,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i (check_conv_record env i appr1 appr2)
+             else conv_record flags env (check_conv_record env i appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
         and f4 i =
           evar_eqappr_x flags env i pbty
@@ -1003,7 +991,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         let f3 i =
           (try
              if not flags.with_cs then raise Not_found
-             else conv_record flags env i (check_conv_record env i appr2 appr1)
+             else conv_record flags env (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
         and f4 i =
           evar_eqappr_x flags env i pbty appr1
@@ -1113,7 +1101,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         | LetIn _, _ -> assert false
       end
 
-and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
+and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
   (* Tries to unify the states
 
         (proji params1 c1 | sk1)   =   (proji params2 (c (?xs:bs)) | sk2)
@@ -1137,7 +1125,6 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk
 
      had to be initially resolved
   *)
-  let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
   if Reductionops.Stack.compare_shape sk1 sk2 then
     let (evd',ks,_,test) =
       List.fold_left
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index be03ced7eb..965cd7de67 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -78,7 +78,7 @@ val check_problems_are_solved : env -> evar_map -> unit
 
 val check_conv_record : env -> evar_map ->
   state -> state ->
-  Univ.ContextSet.t * (constr * constr)
+  evar_map * (constr * constr)
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) *
     (constr Stack.t * constr Stack.t) * constr *
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index de1af62043..21b2137f09 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -35,6 +35,7 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
+open Structures
 open Type_errors
 open Typing
 open Evarutil
@@ -801,8 +802,8 @@ struct
     in
     let app_f =
       match EConstr.kind sigma fj.uj_val with
-      | Const (p, u) when Recordops.is_primitive_projection p ->
-        let p = Option.get @@ Recordops.find_primitive_projection p in
+      | Const (p, u) when PrimitiveProjections.mem p ->
+        let p = Option.get @@ PrimitiveProjections.find_opt p in
         let p = Projection.make p false in
         let npars = Projection.npars p in
         fun n ->
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c31ecc135c..980575abac 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -12,7 +12,7 @@ Cbv
 Find_subterm
 Evardefine
 Evarsolve
-Recordops
+Structures
 Heads
 Evarconv
 Typing
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
deleted file mode 100644
index 83927085e9..0000000000
--- a/pretyping/recordops.mli
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Constr
-
-(** Operations concerning records and canonical structures *)
-
-(** {6 Records } *)
-(** A structure S is a non recursive inductive type with a single
-   constructor (the name of which defaults to Build_S) *)
-
-type proj_kind = {
-  pk_name: Name.t;
-  pk_true_proj: bool;
-  pk_canonical: bool;
-}
-
-type struc_typ = {
-  s_CONST : constructor;
-  s_EXPECTEDPARAM : int;
-  s_PROJKIND : proj_kind list;
-  s_PROJ : Constant.t option list;
-}
-
-val register_structure : struc_typ -> unit
-val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ
-val rebuild_structure : Environ.env -> struc_typ -> struc_typ
-
-(** [lookup_structure isp] returns the struc_typ associated to the
-   inductive path [isp] if it corresponds to a structure, otherwise
-   it fails with [Not_found] *)
-val lookup_structure : inductive -> struc_typ
-
-(** [lookup_projections isp] returns the projections associated to the
-   inductive path [isp] if it corresponds to a structure, otherwise
-   it fails with [Not_found] *)
-val lookup_projections : inductive -> Constant.t option list
-
-(** raise [Not_found] if not a projection *)
-val find_projection_nparams : GlobRef.t -> int
-
-(** raise [Not_found] if not a projection *)
-val find_projection : GlobRef.t -> struc_typ
-
-val is_projection : Constant.t -> bool
-
-(** Sets up the mapping from constants to primitive projections *)
-val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit
-
-val is_primitive_projection : Constant.t -> bool
-
-val find_primitive_projection : Constant.t -> Projection.Repr.t option
-
-(** {6 Canonical structures } *)
-(** A canonical structure declares "canonical" conversion hints between
-    the effective components of a structure and the projections of the
-    structure *)
-
-(** A cs_pattern characterizes the form of a component of canonical structure *)
-type cs_pattern =
-    Const_cs of GlobRef.t
-  | Proj_cs of Projection.Repr.t
-  | Prod_cs
-  | Sort_cs of Sorts.family
-  | Default_cs
-
-type obj_typ = {
-  o_ORIGIN : GlobRef.t;
-  o_DEF : constr;
-  o_CTX : Univ.AUContext.t;
-  o_INJ : int option;      (** position of trivial argument *)
-  o_TABS : constr list;    (** ordered *)
-  o_TPARAMS : constr list; (** ordered *)
-  o_NPARAMS : int;
-  o_TCOMPS : constr list } (** ordered *)
-
-(** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list
-
-val pr_cs_pattern : cs_pattern -> Pp.t
-
-type cs = GlobRef.t * inductive
-
-val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ
-val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
-  cs -> unit
-val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
-val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> EConstr.t -> bool
-val canonical_projections : unit ->
-  ((GlobRef.t * cs_pattern) * obj_typ) list
-
-val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs
diff --git a/pretyping/recordops.ml b/pretyping/structures.ml
index aa862a912e..3ef6e98373 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/structures.ml
@@ -37,71 +37,67 @@ open Reductionops
          * the constant realizing this projection (if any).
 *)
 
-type proj_kind = {
-  pk_name: Name.t;
-  pk_true_proj: bool;
-  pk_canonical: bool;
+module Structure = struct
+
+type projection = {
+  proj_name : Names.Name.t;
+  proj_true : bool;
+  proj_canonical : bool;
+  proj_body : Names.Constant.t option;
+}
+
+type t = {
+  name : Names.inductive;
+  projections : projection list;
+  nparams : int;
 }
 
-type struc_typ = {
-  s_CONST : constructor;
-  s_EXPECTEDPARAM : int;
-  s_PROJKIND : proj_kind list;
-  s_PROJ : Constant.t option list }
+let make env name projections =
+  let nparams = Inductiveops.inductive_nparams env name in
+  { name; projections; nparams }
 
 let structure_table =
-  Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
+  Summary.ref (Indmap.empty : t Indmap.t) ~name:"record-structs"
 let projection_table =
-  Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
+  Summary.ref (Cmap.empty : t Cmap.t) ~name:"record-projs"
 
-let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) =
-  structure_table := Indmap.add ind struc !structure_table;
+let register ({ name; projections; nparams } as s) =
+  structure_table := Indmap.add name s !structure_table;
   projection_table :=
-    List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
-      projs !projection_table
-
-let subst_structure subst struc =
-  let projs' =
-   (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
-   (* the first component of subst_con.                                   *)
-   List.Smart.map
-     (Option.Smart.map (subst_constant subst))
-    struc.s_PROJ
-  in
-  let id' = Globnames.subst_constructor subst struc.s_CONST in
-  if projs' == struc.s_PROJ && id' == struc.s_CONST
-  then struc
-  else { struc with s_CONST = id'; s_PROJ = projs' }
+    List.fold_right (fun { proj_body } m ->
+      Option.fold_right (fun proj -> Cmap.add proj s) proj_body m)
+    projections !projection_table
 
-let rebuild_structure env struc =
-  let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in
-  let npars = mib.Declarations.mind_nparams in
-  { struc with s_EXPECTEDPARAM = npars }
+let subst subst ({ name; projections; nparams } as s) =
+  let subst_projection subst ({ proj_body } as p) =
+    let proj_body = Option.Smart.map (subst_constant subst) proj_body in
+    if proj_body == p.proj_body then p else
+    { p with proj_body } in
+  let projections = List.Smart.map (subst_projection subst) projections in
+  let name = Mod_subst.subst_ind subst name in
+  if projections == s.projections &&
+     name == s.name
+  then s
+  else { name; projections; nparams }
 
-let lookup_structure indsp = Indmap.find indsp !structure_table
+let rebuild env s =
+  let mib = Environ.lookup_mind (fst s.name) env in
+  let nparams = mib.Declarations.mind_nparams in
+  { s with nparams }
 
-let lookup_projections indsp = (lookup_structure indsp).s_PROJ
+let find indsp = Indmap.find indsp !structure_table
 
-let find_projection_nparams = function
-  | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
-  | _ -> raise Not_found
+let find_projections indsp =
+  (find indsp).projections |>
+  List.map (fun { proj_body } -> proj_body)
 
-let find_projection = function
-  | GlobRef.ConstRef cst -> Cmap.find cst !projection_table
-  | _ -> raise Not_found
+let find_from_projection cst = Cmap.find cst !projection_table
 
-let is_projection cst = Cmap.mem cst !projection_table
+let projection_nparams cst = (Cmap.find cst !projection_table).nparams
 
-let prim_table =
-  Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
-
-let register_primitive_projection p c =
-  prim_table := Cmap_env.add c p !prim_table
-
-let is_primitive_projection c = Cmap_env.mem c !prim_table
+let is_projection cst = Cmap.mem cst !projection_table
 
-let find_primitive_projection c =
-  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+end
 
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
@@ -142,49 +138,55 @@ type obj_typ = {
   o_NPARAMS : int;
   o_TCOMPS : constr list } (* ordered *)
 
-type cs_pattern =
+module ValuePattern = struct
+
+type t =
     Const_cs of GlobRef.t
-  | Proj_cs of Projection.Repr.t
+  | Proj_cs of Names.Projection.Repr.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
 
-let eq_cs_pattern env p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
-| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
-| Prod_cs, Prod_cs -> true
-| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
-| Default_cs, Default_cs -> true
-| _ -> false
-
-let rec assoc_pat env a = function
-  | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs
-  | [] -> raise Not_found
-
-
-let object_table =
-  Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t)
-    ~name:"record-canonical-structs"
-
-let canonical_projections () =
-  GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
-    !object_table []
-
-let keep_true_projections projs kinds =
-  let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in
-  List.map_filter filter (List.combine projs kinds)
+let equal env p1 p2 = match p1, p2 with
+  | Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+  | Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
+  | Prod_cs, Prod_cs -> true
+  | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
+  | Default_cs, Default_cs -> true
+  | _ -> false
 
-let rec cs_pattern_of_constr env t =
+let rec of_constr env t =
   match kind t with
   | App (f,vargs) ->
-    let patt, n, args = cs_pattern_of_constr env f in
+    let patt, n, args = of_constr env f in
     patt, n, args @ Array.to_list vargs
   | Rel n -> Default_cs, Some n, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
-  | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c]
+  | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
   | _ -> Const_cs (fst @@ destRef t) , None, []
 
+let print = function
+    Const_cs c -> Nametab.pr_global_env Id.Set.empty c
+  | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Names.Projection.Repr.constant p))
+  | Prod_cs -> str "_ -> _"
+  | Default_cs -> str "_"
+  | Sort_cs s -> Sorts.pr_sort_family s
+
+end
+
+let rec assoc_pat env a = function
+  | ((pat, t), e) :: xs -> if ValuePattern.equal env pat a then (t, e) else assoc_pat env a xs
+  | [] -> raise Not_found
+
+let object_table =
+  Summary.ref (GlobRef.Map.empty : ((ValuePattern.t * constr) * obj_typ) list GlobRef.Map.t)
+    ~name:"record-canonical-structs"
+
+let keep_true_projections projs =
+  let filter { Structure.proj_true ; proj_canonical; proj_body } = if proj_true then Some (proj_body, proj_canonical) else None in
+  List.map_filter filter projs
+
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (sign,env,t,ref,proji_sp) ->
@@ -213,17 +215,17 @@ let compute_canonical_projections env ~warn (gref,ind) =
   let t = EConstr.Unsafe.to_constr t in
   let o_TABS = List.rev_map snd sign in
   let args = snd (decompose_app t) in
-  let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
-    lookup_structure ind in
+  let { Structure.nparams = p; projections = lpj } =
+    Structure.find ind in
   let o_TPARAMS, projs = List.chop p args in
   let o_NPARAMS = List.length o_TPARAMS in
-  let lpj = keep_true_projections lpj kl in
+  let lpj = keep_true_projections lpj in
   let nenv = Termops.push_rels_assum sign env in
   List.fold_left2 (fun acc (spopt, canonical) t ->
       if canonical
       then
         Option.cata (fun proji_sp ->
-            match cs_pattern_of_constr nenv t with
+            match ValuePattern.of_constr nenv t with
             | patt, o_INJ, o_TCOMPS ->
               ((GlobRef.ConstRef proji_sp, (patt, t)),
                { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
@@ -235,13 +237,6 @@ let compute_canonical_projections env ~warn (gref,ind) =
       else acc
     ) [] lpj projs
 
-let pr_cs_pattern = function
-    Const_cs c -> Nametab.pr_global_env Id.Set.empty c
-  | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p))
-  | Prod_cs -> str "_ -> _"
-  | Default_cs -> str "_"
-  | Sort_cs s -> Sorts.pr_sort_family s
-
 let warn_redundant_canonical_projection =
   CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
          (fun (hd_val,prj,new_can_s,old_can_s) ->
@@ -249,26 +244,13 @@ let warn_redundant_canonical_projection =
           ++ strbrk " by " ++ prj ++ strbrk " in "
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
-let register_canonical_structure ~warn env sigma o =
-    compute_canonical_projections env ~warn o |>
-    List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
-      let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
-      match assoc_pat env cs_pat l with
-      | exception Not_found ->
-          object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
-      | _, cs ->
-        if warn
-        then
-          let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
-          let 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 in
-          let hd_val = pr_cs_pattern cs_pat in
-          warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
-      )
+module Instance = struct
 
-type cs = GlobRef.t * inductive
+type t = GlobRef.t * inductive
 
-let subst_canonical_structure subst (gref,ind as obj) =
+let repr = fst
+
+let subst subst (gref,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   match gref with
@@ -286,7 +268,7 @@ let error_not_structure ref description =
        (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
           description))
 
-let check_and_decompose_canonical_structure env sigma ref =
+let make env sigma ref =
   let vc =
     match ref with
     | GlobRef.ConstRef sp ->
@@ -311,17 +293,71 @@ let check_and_decompose_canonical_structure env sigma ref =
     | Construct ((indsp,1),u) -> indsp
     | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
   let s =
-    try lookup_structure indsp
+    try Structure.find indsp
     with Not_found ->
       error_not_structure ref
         (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
-  let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
-  if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
+  let ntrue_projs = List.count (fun { Structure.proj_true = x } -> x) s.Structure.projections in
+  if s.Structure.nparams + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (ref,indsp)
 
-let lookup_canonical_conversion env (proj,pat) =
-  assoc_pat env pat (GlobRef.Map.find proj !object_table)
+let register ~warn env sigma o =
+    compute_canonical_projections env ~warn o |>
+    List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
+      let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
+      match assoc_pat env cs_pat l with
+      | exception Not_found ->
+          object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
+      | _, cs ->
+        if warn
+        then
+          let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
+          let 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 in
+          let hd_val = ValuePattern.print cs_pat in
+          warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
+      )
+
+end
+
+(** The canonical solution of a problem (proj,val) is a global
+    [constant = fun abs : abstractions_ty => body] and
+    [ body = RecodConstructor params canon_values ] and the canonical value
+    corresponding to val is [val cvalue_arguments].
+    It is possible that val is one of the [abs] abstractions, eg [Default_cs],
+    and in that case [cvalue_abstraction = Some i] *)
+
+module CanonicalSolution = struct
+type t = {
+  constant : EConstr.t;
+
+  abstractions_ty : EConstr.t list;
+  body : EConstr.t;
+
+  nparams : int;
+  params : EConstr.t list;
+  cvalue_abstraction : int option;
+  cvalue_arguments : EConstr.t list;
+}
+
+let find env sigma (proj,pat) =
+  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
+        o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = assoc_pat env pat (GlobRef.Map.find proj !object_table) in
+  let us = List.map EConstr.of_constr us in
+  let params = List.map EConstr.of_constr params in
+  let u, ctx' = UnivGen.fresh_instance_from ctx None in
+  let subst = Univ.make_inverse_instance_subst u in
+  let c = EConstr.of_constr c in
+  let c' = EConstr.Vars.subst_univs_level_constr subst c in
+  let t' = EConstr.of_constr t' in
+  let t' = EConstr.Vars.subst_univs_level_constr subst t' in
+  let bs' = List.map (EConstr.of_constr %> EConstr.Vars.subst_univs_level_constr subst) bs in
+  let params = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) params in
+  let us = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) us in
+  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
+  sigma, { body = t'; constant = c'; abstractions_ty = bs'; nparams; params; cvalue_arguments = us; cvalue_abstraction = n }
+
 
 let rec get_nth n = function
 | [] -> raise Not_found
@@ -336,12 +372,12 @@ let rec decompose_projection sigma c args =
   | Cast (c, _, _) -> decompose_projection sigma c args
   | App (c, arg) -> decompose_projection sigma c (arg :: args)
   | Const (c, u) ->
-     let n = find_projection_nparams (GlobRef.ConstRef c) in
+     let n = Structure.projection_nparams c in
      (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
      get_nth n args
   | Proj (p, c) ->
-     let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
+     let _ = GlobRef.Map.find (GlobRef.ConstRef (Names.Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
@@ -355,3 +391,44 @@ let is_open_canonical_projection env sigma c =
       not (isConstruct sigma hd)
     with Failure _ -> false
   with Not_found -> false
+
+end
+
+module CSTable = struct
+
+type entry = {
+  projection : Names.GlobRef.t;
+  value : ValuePattern.t;
+  solution : Names.GlobRef.t;
+}
+
+let canonical_entry_of_object projection ((value,_), { o_ORIGIN = solution }) =
+  { projection; value; solution }
+
+let entries () =
+  GlobRef.Map.fold (fun p ol acc ->
+    List.fold_right (fun o acc -> canonical_entry_of_object p o :: acc) ol acc)
+    !object_table []
+
+let entries_for ~projection:p =
+  try
+    GlobRef.Map.find p !object_table |>
+    List.map (canonical_entry_of_object p)
+  with Not_found -> []
+
+end
+
+module PrimitiveProjections = struct
+
+let prim_table =
+  Summary.ref (Cmap_env.empty : Names.Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
+
+let register p c =
+  prim_table := Cmap_env.add c p !prim_table
+
+let mem c = Cmap_env.mem c !prim_table
+
+let find_opt c =
+  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+
+end
diff --git a/pretyping/structures.mli b/pretyping/structures.mli
new file mode 100644
index 0000000000..a1cc38e8e0
--- /dev/null
+++ b/pretyping/structures.mli
@@ -0,0 +1,163 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+
+(** A structure S is a non recursive inductive type with a single
+   constructor *)
+module Structure : sig
+
+(** A projection to a structure field *)
+type projection = {
+  proj_name : Names.Name.t;            (** field name *)
+  proj_true : bool;                    (** false for primitive records *)
+  proj_canonical : bool;               (** false = not to be used for CS inference *)
+  proj_body : Names.Constant.t option; (** the projection function *)
+}
+
+type t = {
+  name : Names.inductive;
+  projections : projection list;
+  nparams : int;
+}
+
+val make : Environ.env -> Names.inductive -> projection list -> t
+
+val register : t -> unit
+val subst : Mod_subst.substitution -> t -> t
+
+(** refreshes nparams, e.g. after section discharging *)
+val rebuild : Environ.env -> t -> t
+
+(** [find isp] returns the Structure.t associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val find : Names.inductive -> t
+
+(** raise [Not_found] if not a structure projection *)
+val find_from_projection : Names.Constant.t -> t
+
+(** [lookup_projections isp] returns the projections associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val find_projections : Names.inductive -> Names.Constant.t option list
+
+(** raise [Not_found] if not a projection *)
+val projection_nparams : Names.Constant.t -> int
+
+val is_projection : Names.Constant.t -> bool
+
+end
+
+(** A canonical instance declares "canonical" conversion hints between
+    the effective components of a structure and the projections of the
+    structure *)
+module Instance : sig
+
+type t
+
+(** Process a record instance, checkig it can be registered as canonical.
+    The record type must be declared as a canonical Structure.t beforehand.  *)
+val make : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t
+
+(** Register an instance as canonical *)
+val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit
+
+val subst : Mod_subst.substitution -> t -> t
+val repr : t -> Names.GlobRef.t
+
+end
+
+
+(** A ValuePattern.t characterizes the form of a component of canonical
+    instance and is used to query the data base of canonical instances *)
+module ValuePattern : sig
+
+type t =
+  | Const_cs of Names.GlobRef.t
+  | Proj_cs of Names.Projection.Repr.t
+  | Prod_cs
+  | Sort_cs of Sorts.family
+  | Default_cs
+
+val equal : Environ.env -> t -> t -> bool
+val print : t -> Pp.t
+
+(** Return the form of the component of a canonical structure *)
+val of_constr : Environ.env -> Constr.t -> t * int option * Constr.t list
+
+end
+
+
+(** The canonical solution of a problem (proj,val) is a global
+    [constant = fun abs : abstractions_ty => body] and
+    [body = RecodConstructor params canon_values] and the canonical value
+    corresponding to val is [val cvalue_arguments].
+    It is possible that val is one of the [abs] abstractions, eg [Default_cs],
+    and in that case [cvalue_abstraction = Some i] *)
+
+module CanonicalSolution : sig
+
+type t = {
+  constant : EConstr.t;
+
+  abstractions_ty : EConstr.t list;
+  body : EConstr.t;
+
+  nparams : int;
+  params : EConstr.t list;
+  cvalue_abstraction : int option;
+  cvalue_arguments : EConstr.t list;
+}
+
+(** [find (p,v)] returns a s such that p s = v.
+    The solution s gets a fresh universe instance and is decomposed into
+    bits for consumption by evarconv. Can raise [Not_found] on failure *)
+val find :
+  Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) ->
+    Evd.evar_map * t
+
+(** [is_open_canonical_projection env sigma t] is true if t is a FieldName
+    applied to term which is not a constructor. Used by evarconv not to
+    unfold too much and lose a projection too early *)
+val is_open_canonical_projection :
+  Environ.env -> Evd.evar_map -> EConstr.t -> bool
+
+end
+
+(** Low level access to the Canonical Structure database *)
+module CSTable : sig
+
+type entry = {
+  projection : Names.GlobRef.t;
+  value : ValuePattern.t;
+  solution : Names.GlobRef.t;
+}
+
+(** [all] returns the list of tuples { p ; v ; s }
+   Note: p s = v *)
+val entries : unit -> entry list
+
+(** [entries_for p] returns the list of canonical entries that have
+    p as their FieldName *)
+val entries_for : projection:Names.GlobRef.t -> entry list
+
+end
+
+(** Some extra info for structures which are primitive records *)
+module PrimitiveProjections : sig
+
+(** Sets up the mapping from constants to primitive projections *)
+val register : Names.Projection.Repr.t -> Names.Constant.t -> unit
+
+val mem : Names.Constant.t -> bool
+
+val find_opt : Names.Constant.t -> Names.Projection.Repr.t option
+
+end
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index df0f49a033..18db75eed5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -22,13 +22,13 @@ open Namegen
 open Evd
 open Reduction
 open Reductionops
+open Structures
 open Evarutil
 open Evardefine
 open Evarsolve
 open Pretype_errors
 open Retyping
 open Coercion
-open Recordops
 open Locus
 open Locusops
 open Find_subterm
@@ -509,13 +509,13 @@ let key_of env sigma b flags f =
   match EConstr.kind sigma f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
       (TransparentState.is_transparent_constant flags.modulo_delta cst
-       || Recordops.is_primitive_projection cst) ->
+       || PrimitiveProjections.mem cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) &&
       TransparentState.is_transparent_variable flags.modulo_delta id ->
     Some (IsKey (VarKey id))
-  | Proj (p, c) when Projection.unfolded p
+  | Proj (p, c) when Names.Projection.unfolded p
     || (is_transparent env (ConstKey (Projection.constant p)) &&
        (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
     Some (IsProj (p, c))
@@ -1077,7 +1077,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-          if is_open_canonical_projection curenv sigma cM then
+          if CanonicalSolution.is_open_canonical_projection curenv sigma cM then
             solve_canonical_projection curenvnb pb opt cM cN substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1091,7 +1091,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-              if is_open_canonical_projection curenv sigma cN then
+              if CanonicalSolution.is_open_canonical_projection curenv sigma cN then
                 solve_canonical_projection curenvnb pb opt cN cM substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1099,12 +1099,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
     let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
     let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
-    let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+    let (sigma,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
     if Reductionops.Stack.compare_shape ts ts1 then
-      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
       let (evd,ks,_) =
         List.fold_left
           (fun (evd,ks,m) b ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5e9c3baeb1..31b276bb3e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -320,7 +320,7 @@ let strip_params env sigma c =
   | App (f, args) ->
     (match EConstr.kind sigma f with
     | Const (cst,_) ->
-      (match Recordops.find_primitive_projection cst with
+      (match Structures.PrimitiveProjections.find_opt cst with
        | Some p ->
          let p = Projection.make p false in
          let npars = Projection.npars p in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 67bf8d0d29..decf19588f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1555,7 +1555,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | Some proj ->
           let args = Context.Rel.to_extended_vect mkRel 0 sign in
           let proj =
-            match Recordops.find_primitive_projection proj with
+            match Structures.PrimitiveProjections.find_opt proj with
             | Some proj ->
               mkProj (Projection.make proj false, mkApp (c, args))
             | None ->
@@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
         let params = List.map EConstr.of_constr params in
         let cstr = (get_constructors env indf).(0) in
         let elim =
-          try DefinedRecord (Recordops.lookup_projections ind)
+          try DefinedRecord (Structures.Structure.find_projections ind)
           with Not_found ->
             let u = EInstance.kind sigma u in
             let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index eaa6c84791..2c04032ca0 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -7,30 +7,30 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-open Names
 open Libobject
-open Recordops
+open Structures
 
 let open_canonical_structure i (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
+  if Int.equal i 1 then Instance.register env sigma ~warn:false o
 
 let cache_canonical_structure (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  register_canonical_structure ~warn:true env sigma o
+  Instance.register ~warn:true env sigma o
 
-let discharge_canonical_structure (_,((gref, _ as x), local)) =
+let discharge_canonical_structure (_,(x, local)) =
+  let gref = Instance.repr x in
   if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
   else Some (x, local)
 
 
-let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
+let inCanonStruc : Instance.t * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
                   open_function = simple_open open_canonical_structure;
                   cache_function = cache_canonical_structure;
-                  subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
+                  subst_function = (fun (subst,(c,local)) -> Instance.subst subst c, local);
                   classify_function = (fun x -> Substitute x);
                   discharge_function = discharge_canonical_structure }
 
@@ -39,4 +39,4 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 let declare_canonical_structure ?(local=false) ref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref, local)
+  add_canonical_structure (Instance.make env sigma ref, local)
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 86b15739f9..26d696ff8e 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -90,7 +90,7 @@ let uniform_cond sigma ctx lt =
 
 let class_of_global = function
   | GlobRef.ConstRef sp ->
-    (match Recordops.find_primitive_projection sp with
+    (match Structures.PrimitiveProjections.find_opt sp with
      | Some p -> CL_PROJ p | None -> CL_CONST sp)
   | GlobRef.IndRef sp -> CL_IND sp
   | GlobRef.VarRef id -> CL_SECVAR id
@@ -141,8 +141,8 @@ let get_target env t ind =
     CL_FUN
   else
     match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with
-    | CL_CONST p when Recordops.is_primitive_projection p ->
-      CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
+    | CL_CONST p when Structures.PrimitiveProjections.mem p ->
+      CL_PROJ (Option.get @@ Structures.PrimitiveProjections.find_opt p)
     | x -> x
 
 let strength_of_cl = function
@@ -265,7 +265,7 @@ let inCoercion : coe_info_typ -> obj =
 let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
   let isproj =
     match coef with
-    | GlobRef.ConstRef c -> Recordops.find_primitive_projection c
+    | GlobRef.ConstRef c -> Structures.PrimitiveProjections.find_opt c
     | _ -> None
   in
   let c = {
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 1b811f3db7..39520a68ec 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -41,8 +41,8 @@ let kind_searcher = Decls.(function
     Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr &&
                                       (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions)
   | IsDefinition CanonicalStructure ->
-    let canonproj = Recordops.canonical_projections () in
-    Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj)
+    let canonproj = Structures.CSTable.entries () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Structures.CSTable.solution gr) canonproj)
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
     Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes)
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 7050ddc042..2ab6e3bb15 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -76,7 +76,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag =
 
 let inInductive v = Libobject.Dyn.Easy.inj v objInductive
 
-let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+let cache_prim (_,(p,c)) = Structures.PrimitiveProjections.register p c
 
 let load_prim _ p = cache_prim p
 
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ec6e3b44ba..a3cd7a8edc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -24,7 +24,6 @@ open Impargs
 open Libobject
 open Libnames
 open Globnames
-open Recordops
 open Printer
 open Printmod
 open Context.Rel.Declaration
@@ -1005,22 +1004,24 @@ let print_path_between cls clt =
   print_path ((cls, clt), p)
 
 let print_canonical_projections env sigma grefs =
-  let match_proj_gref ((x,y),c) gr =
-    GlobRef.equal x gr ||
-    begin match y with
-      | Const_cs y -> GlobRef.equal y gr
+  let open Structures in
+  let match_proj_gref { CSTable.projection; value; solution } gr =
+    GlobRef.equal projection gr ||
+    begin match value with
+      | ValuePattern.Const_cs y -> GlobRef.equal y gr
       | _ -> false
     end ||
-    GlobRef.equal c.o_ORIGIN gr
+    GlobRef.equal solution gr
   in
   let projs =
     List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
-      (canonical_projections ())
+      (CSTable.entries ())
   in
   prlist_with_sep fnl
-    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+    (fun { CSTable.projection; value; solution } ->
+    ValuePattern.print value ++
     str " <- " ++
-    pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
+    pr_global projection ++ str " ( " ++ pr_global solution ++ str " )")
     projs
 
 (*************************************************************************)
diff --git a/vernac/record.ml b/vernac/record.ml
index ff6bdc5199..fccc3e4fbd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -22,6 +22,7 @@ open Type_errors
 open Constrexpr
 open Constrexpr_ops
 open Context.Rel.Declaration
+open Structures
 
 module RelDecl = Context.Rel.Declaration
 
@@ -348,7 +349,7 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
    this could be refactored as noted above by moving to the
    higher-level declare constant API *)
 let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls
-    paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp =
+    paramargs decl impls fid subst nfi ti i indsp mib lifted_fields x rp =
   let ccl = subst_projection fid subst ti in
   let body, p_opt = match decl with
     | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
@@ -396,32 +397,33 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
     ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
   end;
   let i = if is_local_assum decl then i+1 else i in
-  (Some kn::sp_projs, i, Projection term::subst)
+  (Some kn, i, Projection term::subst)
 
 (** [build_proj] will build a projection for each field, or skip if
    the field is anonymous, i.e. [_ : t] *)
 let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs
-    (nfi,i,kinds,sp_projs,subst) flags decl impls =
+    (nfi,i,kinds,subst) flags decl impls =
   let fi = RelDecl.get_name decl in
   let ti = RelDecl.get_type decl in
-  let (sp_projs,i,subst) =
+  let (sp_proj,i,subst) =
     match fi with
     | Anonymous ->
-      (None::sp_projs,i,NoProjection fi::subst)
+      (None,i,NoProjection fi::subst)
     | Name fid ->
       try build_named_proj
             ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid
-            subst sp_projs nfi ti i indsp mib lifted_fields x rp
+            subst nfi ti i indsp mib lifted_fields x rp
       with NotDefinable why as exn ->
         let _, info = Exninfo.capture exn in
         warning_or_error ~info flags.pf_subclass indsp why;
-        (None::sp_projs,i,NoProjection fi::subst)
+        (None,i,NoProjection fi::subst)
   in
   (nfi - 1, i,
-   { Recordops.pk_name = fi
-   ; pk_true_proj = is_local_assum decl
-   ; pk_canonical = flags.pf_canonical } :: kinds
-  , sp_projs, subst)
+   { Structure.proj_name = fi
+   ; proj_true = is_local_assum decl
+   ; proj_canonical = flags.pf_canonical
+   ; proj_body = sp_proj } :: kinds
+  , subst)
 
 (** [declare_projections] prepares the common context for all record
    projections and then calls [build_proj] for each one. *)
@@ -445,11 +447,12 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name
     | PrimRecord _ -> true
     | FakeRecord | NotRecord -> false
   in
-  let (_,_,kinds,sp_projs,_) =
+  let (_,_,canonical_projections,_) =
     List.fold_left3
       (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs)
-      (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
-  in (kinds,sp_projs)
+      (List.length fields,0,[],[]) flags (List.rev fields) (List.rev fieldimpls)
+  in
+    List.rev canonical_projections
 
 open Typeclasses
 
@@ -485,20 +488,17 @@ let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min
     (* auto detect template *)
     ComInductive.should_auto_template id (template && template_candidate ())
 
-let load_structure i (_, structure) =
-  Recordops.register_structure structure
+let load_structure i (_, structure) = Structure.register structure
 
-let cache_structure o =
-  load_structure 1 o
+let cache_structure o = load_structure 1 o
 
-let subst_structure (subst, obj) =
-  Recordops.subst_structure subst obj
+let subst_structure (subst, obj) = Structure.subst subst obj
 
 let discharge_structure (_, x) = Some x
 
-let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
+let rebuild_structure s = Structure.rebuild (Global.env()) s
 
-let inStruc : Recordops.struc_typ -> Libobject.obj =
+let inStruc : Structure.t -> Libobject.obj =
   let open Libobject in
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
@@ -601,17 +601,10 @@ let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls par
   let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
-    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in
+    let projections = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in
     let build = GlobRef.ConstructRef cstr in
     let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
-    let npars = Inductiveops.inductive_nparams (Global.env()) rsp in
-    let struc = {
-      Recordops.s_CONST = cstr;
-      s_PROJ = List.rev sp_projs;
-      s_PROJKIND = List.rev kinds;
-      s_EXPECTEDPARAM = npars;
-    }
-    in
+    let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
     rsp
   in
@@ -674,7 +667,7 @@ let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
       meth_info = b;
       meth_const = y;
     } in
-    let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
+    let l = List.map3 map (List.rev fields) coers (Structure.find_projections ind) in
     GlobRef.IndRef ind, l
   in
   List.map map inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 7a40af048c..feb257da3c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -11,6 +11,7 @@
 open Names
 open Vernacexpr
 open Constrexpr
+open Structures
 
 module Ast : sig
   type t =
@@ -51,8 +52,8 @@ module Internal : sig
     -> projection_flags list
     -> Impargs.manual_implicits list
     -> Constr.rel_context
-    -> Recordops.proj_kind list * Names.Constant.t option list
+    -> Structure.projection list
 
-  val declare_structure_entry : Recordops.struc_typ -> unit
+  val declare_structure_entry : Structure.t -> unit
 
 end