From c3de822e711fa3f10817432b7023fc2f88c0aeeb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 20:41:17 +0100
Subject: Making Evarutil independent from Reductionops.

---
 tactics/hints.ml   | 2 +-
 tactics/rewrite.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 730da147af..e5abad6863 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1072,7 +1072,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   let c' = iter c in
-    if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 4c06550d44..fb04bee070 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1880,7 +1880,7 @@ let build_morphism_signature m =
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let m = Evarutil.nf_evar evd morph in
-    Evarutil.check_evars env Evd.empty evd m; m
+    Pretyping.check_evars env Evd.empty evd m; m
 
 let default_morphism sign m =
   let env = Global.env () in
-- 
cgit v1.2.3