Rename types_or_terms and the unification function types

1 files changed, 20 insertions, 9 deletions

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 94f17de6cc..87804f01b6 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -40,15 +40,26 @@ val expand_vars_in_term : env -> evar_map -> constr -> constr
    some problems that cannot be solved in a unique way (except if choose is
    true); fails if the instance is not valid for the given [ev] *)
 
-type types_or_terms = bool
+(** One might want to use different conversion strategies for types and terms:
+    e.g. preventing delta reductions when doing term unifications but allowing
+    arbitrary delta conversion when checking the types of evar instances. *)
 
-type conv_fun = types_or_terms ->
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(** A unification function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to unify. *)
+type unifier = unification_kind ->
   env -> evar_map -> conv_pb -> constr -> constr -> unification_result
 
-type conv_fun_bool = types_or_terms ->
+(** A conversion function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to convert.
+    Conversion is not allowed to instantiate evars contrary to unification. *)
+type conversion_check = unification_kind ->
   env ->  evar_map -> conv_pb -> constr -> constr -> bool
 
-val evar_define : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool ->
+val evar_define : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool ->
   env -> evar_map -> bool option -> existential -> constr -> evar_map
 
 val refresh_universes :
@@ -60,18 +71,18 @@ val refresh_universes :
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-val solve_refl : ?can_drop:bool -> unify_flags -> conv_fun_bool -> env ->  evar_map ->
+val solve_refl : ?can_drop:bool -> unify_flags -> conversion_check -> env ->  evar_map ->
   bool option -> Evar.t -> constr array -> constr array -> evar_map
 
 val solve_evar_evar : ?force:bool -> unify_flags ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
-  conv_fun ->
+  unifier ->
   env ->  evar_map -> bool option -> existential -> existential -> evar_map
 
-val solve_simple_eqn : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
+val solve_simple_eqn : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
-val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+val reconsider_unif_constraints : unifier -> evar_map -> unification_result
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
@@ -87,7 +98,7 @@ exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
 val check_evar_instance :
-  evar_map -> Evar.t -> constr -> conv_fun -> evar_map
+  evar_map -> Evar.t -> constr -> unifier -> evar_map
 
 val remove_instance_local_defs :
   evar_map -> Evar.t -> 'a array -> 'a list