Setup hook to change the unification algorithm used by evarconv,

e.g. for MTac.

1 files changed, 10 insertions, 0 deletions

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) =