Setup hook to change the unification algorithm used by evarconv,

e.g. for MTac.

3 files changed, 20 insertions, 8 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ae9210e494..de6b177b83 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -506,12 +506,6 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
       	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
 	  with NoCoercionNoUnifier (best_failed_evd,e) ->
 	    error_actual_type_loc loc env best_failed_evd cj t e
-
-	(* let evd = saturate_evd env evd in *)
-      	(*   try *)
-      	(*     inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t *)
-	(*   with NoCoercionNoUnifier (best_failed_evd,e) -> *)
-	    (* error_actual_type_loc loc env best_failed_evd cj t e *)
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 55fd23aa51..f217be7dd1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -23,6 +23,9 @@ open Globnames
 open Evd
 open Pretype_errors
 
+type unify_fun = transparent_state ->
+  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
@@ -845,6 +848,13 @@ let evar_conv_x =
       Profile.profile6 evar_conv_xkey evar_conv_x
   else evar_conv_x
 
+let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
+
+let evar_conv_x ts = Hook.get evar_conv_hook_get ts
+
+let set_evar_conv f = Hook.set evar_conv_hook_set f
+
+
 (* We assume here |l1| <= |l2| *)
 
 let first_order_unification ts env evd (ev1,l1) (term2,l2) =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 12cf7d0b73..f3363e3587 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -59,12 +59,20 @@ val second_order_matching : transparent_state -> env -> evar_map ->
 
 val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
 
+type unify_fun = transparent_state ->
+  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+
+(** Override default [evar_conv_x] algorithm. *)
+val set_evar_conv : unify_fun -> unit
+
+(** The default unification algorithm with evars and universes. *)
+val evar_conv_x : unify_fun
+
 (**/**)
 (* For debugging *)
-val evar_conv_x : transparent_state ->
-  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
   env -> evar_map ->
     conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
       Evarsolve.unification_result
 (**/**)
+