diff --git a/engine/evd.ml b/engine/evd.ml
index 0e19a29716cf..b223f3178bb6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -892,6 +892,8 @@ let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
 
 let undefined_map d = d.undf_evars
 
+let defined_map d = d.defn_evars
+
 let drop_all_defined d = { d with defn_evars = EvMap.empty }
 
 (* spiwack: not clear what folding over an evar_map, for now we shall
diff --git a/engine/evd.mli b/engine/evd.mli
index 43c9cc45349c..59718ff92990 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -277,6 +277,9 @@ val add_quconstraints : evar_map -> Sorts.QUConstraints.t -> evar_map
 val undefined_map : evar_map -> undefined evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
+val defined_map : evar_map -> defined evar_info Evar.Map.t
+(** Access the defined evar mapping directly. *)
+
 val drop_all_defined : evar_map -> evar_map
 
 val drop_new_defined : original:evar_map -> evar_map -> evar_map
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
index 239d2491e9e4..c8aa2c82df8e 100644
--- a/pretyping/structures.ml
+++ b/pretyping/structures.ml
@@ -97,6 +97,11 @@ let projection_nparams cst = (Cmap.find cst !projection_table).nparams
 
 let is_projection cst = Cmap.mem cst !projection_table
 
+let projection_number env cst =
+  let s = find_from_projection cst in
+  CList.index0 (Option.equal (Environ.QConstant.equal env)) (Some cst)
+    (List.map (fun x -> x.proj_body) s.projections)
+
 end
 
 (************************************************************************)
@@ -397,6 +402,18 @@ let is_open_canonical_projection env sigma c =
     with Failure _ -> false
   with Not_found -> false
 
+let print env sigma s =
+  let pr_econstr = Termops.Internal.debug_print_constr sigma in
+  let pr_econstr_list l = Pp.(str "[ " ++ prlist_with_sep (fun () -> str "; ") pr_econstr l ++ str " ]") in
+  Pp.(str "{ constant = " ++ pr_econstr s.constant ++ cut () ++
+     str "abstractions_ty = " ++ pr_econstr_list s.abstractions_ty ++ cut () ++
+     str "body = " ++ pr_econstr s.body ++ cut () ++
+     str "nparams = " ++ int s.nparams ++ cut () ++
+     str "params = " ++ pr_econstr_list s.params ++ cut () ++
+     str "cvalue_abstractions = " ++ pr_opt int s.cvalue_abstraction ++ cut () ++
+     str "cvalue_arguments = " ++ pr_econstr_list s.cvalue_arguments ++ cut () ++
+     str "}")
+
 end
 
 module CSTable = struct
diff --git a/pretyping/structures.mli b/pretyping/structures.mli
index f93682f73c23..5fc6e67e9be5 100644
--- a/pretyping/structures.mli
+++ b/pretyping/structures.mli
@@ -53,6 +53,10 @@ val projection_nparams : Names.Constant.t -> int
 
 val is_projection : Names.Constant.t -> bool
 
+val projection_number : Environ.env -> Names.Constant.t -> int
+(** [projection_number env p] returns the position of the projection p in
+    the structure it corresponds to, counting from 0. *)
+
 end
 
 (** A canonical instance declares "canonical" conversion hints between
@@ -129,6 +133,8 @@ val find :
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> EConstr.t -> bool
 
+val print : Environ.env -> Evd.evar_map -> t -> Pp.t
+
 end
 
 (** Low level access to the Canonical Structure database *)