Merge PR #9909: Remove all but one call to `Global` in the pretyper

Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 14 insertions, 4 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index bd468e62ad..c04182930e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -75,9 +75,19 @@ val inductive_class_of : inductive -> cl_index
 val class_args_of : env -> evar_map -> types -> constr list
 
 (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-val declare_coercion :
-  coe_typ -> ?local:bool -> isid:bool ->
-      src:cl_typ -> target:cl_typ -> params:int -> unit
+type coercion = {
+  coercion_type   : coe_typ;
+  coercion_local  : bool;
+  coercion_is_id  : bool;
+  coercion_is_proj  : Projection.Repr.t option;
+  coercion_source : cl_typ;
+  coercion_target : cl_typ;
+  coercion_params : int;
+}
+
+val subst_coercion : substitution -> coercion -> coercion
+
+val declare_coercion : env -> evar_map -> coercion -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
@@ -101,7 +111,7 @@ val lookup_pattern_path_between :
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)