1 files changed, 45 insertions, 27 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5b416a99f9..3b918b5396 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open CErrors
 open Util
 open Pp
 open Names
-open Globnames
 open Constr
 open Mod_subst
 open Reductionops
@@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) =
      (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = subst_constructor subst id in
+  let id' = Globnames.subst_constructor subst id in
   if projs' == projs && id' == id then obj else
     (id',kl,projs')
 
@@ -114,7 +113,7 @@ let find_primitive_projection c =
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)
 
-(* Table des definitions "object" : pour chaque object c,
+(* Table of "object" definitions: for each object c,
 
   c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
 
@@ -127,16 +126,19 @@ let find_primitive_projection c =
 
   that maps the pair (Li,ci) to the following data
 
+    o_ORIGIN = c (the constant name which this conversion rule is
+                  synthesized from)
     o_DEF = c
     o_TABS = B1...Bk
     o_INJ = Some n        (when ci is a reference to the parameter xi)
-    o_PARAMS = a1...am
-    o_NARAMS = m
+    o_TPARAMS = a1...am
+    o_NPARAMS = m
     o_TCOMP = ui1...uir
 
 *)
 
 type obj_typ = {
+  o_ORIGIN : GlobRef.t;
   o_DEF : constr;
   o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (* position of trivial argument if any *)
@@ -187,13 +189,13 @@ let rec cs_pattern_of_constr env t =
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
-  | _ -> Const_cs (global_of_constr t) , None, []
+  | _ -> Const_cs (Globnames.global_of_constr t) , None, []
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (sign,env,t,con,proji_sp) ->
+         (fun (sign,env,t,ref,proji_sp) ->
           let env = Termops.push_rels_assum sign env in
-          let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in
+          let con_pp = Nametab.pr_global_env Id.Set.empty ref in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) 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: "
@@ -201,11 +203,17 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections env ~warn (con,ind) =
-  let o_CTX = Environ.constant_context env con in
-  let u = Univ.make_abstract_instance o_CTX in
-  let o_DEF = mkConstU (con, u) in
-  let c = Environ.constant_value_in env (con,u) in
+let compute_canonical_projections env ~warn (gref,ind) =
+  let o_CTX = Environ.universes_of_global env gref in
+  let o_DEF, c =
+    match gref with
+    | GlobRef.ConstRef con ->
+        let u = Univ.make_abstract_instance o_CTX in
+        mkConstU (con, u), Environ.constant_value_in env (con,u)
+    | GlobRef.VarRef id ->
+        mkVar id, Option.get (Environ.named_body id env)
+    | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false
+  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
@@ -224,10 +232,10 @@ let compute_canonical_projections env ~warn (con,ind) =
             match cs_pattern_of_constr nenv t with
             | patt, o_INJ, o_TCOMPS ->
               ((GlobRef.ConstRef proji_sp, (patt, t)),
-               { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+               { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
               :: acc
             | exception Not_found ->
-              if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+              if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
               acc
           ) acc spopt
       else acc
@@ -263,12 +271,17 @@ let register_canonical_structure ~warn env sigma o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
-let subst_canonical_structure subst (cst,ind as obj) =
+type cs = GlobRef.t * inductive
+
+let subst_canonical_structure subst (gref,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
-  let cst' = subst_constant subst cst in
-  let ind' = subst_ind subst ind in
-  if cst' == cst && ind' == ind then obj else (cst',ind')
+  match gref with
+  | GlobRef.ConstRef cst ->
+      let cst' = subst_constant subst cst in
+      let ind' = subst_ind subst ind in
+      if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind')
+  | _ -> assert false
 
 (*s High-level declaration of a canonical structure *)
 
@@ -279,15 +292,20 @@ let error_not_structure ref description =
           description))
 
 let check_and_decompose_canonical_structure env sigma ref =
-  let sp =
+  let vc =
     match ref with
-      GlobRef.ConstRef sp -> sp
-    |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
+    | GlobRef.ConstRef sp ->
+        let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
+        begin match Environ.constant_opt_value_in env (sp, u) with
+        | Some vc -> vc
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.VarRef id ->
+        begin match Environ.named_body id env with
+        | Some b -> b
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.IndRef _ | GlobRef.ConstructRef _ ->
+        error_not_structure ref (str "Expected an instance of a record or structure.")
   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 (str "Could not find its value in the global environment.") in
   let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
@@ -305,7 +323,7 @@ let check_and_decompose_canonical_structure env sigma ref =
   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
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
-  (sp,indsp)
+  (ref,indsp)
 
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (GlobRef.Map.find proj !object_table)