8 files changed, 18 insertions, 10 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f0e73bdb29..c980d204ca 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -27,7 +27,7 @@ open EConstr
 open Vars
 open Reductionops
 open Pretype_errors
-open Classops
+open Coercionops
 open Evarutil
 open Evarconv
 open Evd
diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml
index 16021b66f8..16021b66f8 100644
--- a/pretyping/classops.ml
+++ b/pretyping/coercionops.ml
diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli
index 9f633843eb..9f633843eb 100644
--- a/pretyping/classops.mli
+++ b/pretyping/coercionops.mli
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 862865bd90..037006bc47 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -455,7 +455,9 @@ let rec decomp_branch tags nal flags (avoid,env as e) sigma c =
       (avoid', add_name_opt na' body t env) sigma c
 
 let rec build_tree na isgoal e sigma ci cl =
-  let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
+  let mkpat n rhs pl =
+    let na = update_name sigma na rhs in
+    na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in
   let cnl = ci.ci_pp_info.cstr_tags in
   List.flatten
     (List.init (Array.length cl)
@@ -485,7 +487,9 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
   let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
-  List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat
+  List.map (fun (ids,hd,rhs) ->
+      let na, pat = mkpat rhs hd in
+      (Nameops.Name.fold_right Id.Set.add na ids, pat, rhs)) mat
 
 (**********************************************************************)
 (* Transform internal representation of pattern-matching into list of *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0364e1b61f..bfdb471c46 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c =
   (sigma, c)
 
 let path_convertible env sigma i p q =
-  let open Classops in
+  let open Coercionops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
   let mkGApp(rt,rtl)      = DAst.make @@ Glob_term.GApp(rt,rtl) in
@@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q =
       let _ = Evarconv.unify_delay env sigma tp tq in true
   with Evarconv.UnableToUnify _ | PretypeError _ -> false
 
-let _ = Classops.install_path_comparator path_convertible
+let _ = Coercionops.install_path_comparator path_convertible
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 7e140f4399..07154d4e03 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -26,7 +26,7 @@ Constr_matching
 Tacred
 Typeclasses_errors
 Typeclasses
-Classops
+Coercionops
 Program
 Coercion
 Detyping
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5b416a99f9..35e182840b 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,7 +114,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 +127,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 : Constant.t;
   o_DEF : constr;
   o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (* position of trivial argument if any *)
@@ -224,7 +227,7 @@ 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 = con ; 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);
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e8b0d771aa..aaba7cc3e5 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -73,6 +73,7 @@ type cs_pattern =
   | Default_cs
 
 type obj_typ = {
+  o_ORIGIN : Constant.t;
   o_DEF : constr;
   o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (** position of trivial argument *)