Making Evarutil independent from Reductionops.

3 files changed, 15 insertions, 6 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4bf0450d2..2fc0f5ff1 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -191,7 +191,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
 	    nf t
 	in
-	Evarutil.check_evars env Evd.empty !evars termtype;
+	Pretyping.check_evars env Evd.empty !evars termtype;
 	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
@@ -287,7 +287,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       let evm, nf = Evarutil.nf_evar_map_universes !evars in
       let termtype = nf termtype in
       let _ = (* Check that the type is free of evars now. *)
-	Evarutil.check_evars env Evd.empty evm termtype
+	Pretyping.check_evars env Evd.empty evm termtype
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
@@ -361,7 +361,7 @@ let context poly l =
   let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.Rel.map subst fullctx in
-  let ce t = Evarutil.check_evars env Evd.empty !evars t in
+  let ce t = Pretyping.check_evars env Evd.empty !evars t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 31730865f..ad848ccfc 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -76,6 +76,15 @@ let rec contract3' env a b c = function
       let y,x = contract3' env a b c x in
       y,CannotSolveConstraint ((pb,env,t,u),x)
 
+(** Ad-hoc reductions *)
+
+let j_nf_betaiotaevar sigma j =
+  { uj_val = Evarutil.nf_evar sigma j.uj_val;
+    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
+
 (** Printers *)
 
 let pr_lconstr c = quote (pr_lconstr c)
@@ -322,7 +331,7 @@ let explain_unification_error env sigma p1 p2 = function
 
 let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env in
-  let j = Evarutil.j_nf_betaiotaevar sigma j in
+  let j = j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma t in
   (** Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
@@ -337,7 +346,7 @@ let explain_actual_type env sigma j t reason =
   ppreason ++ str ".")
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
-  let randl = Evarutil.jv_nf_betaiotaevar sigma randl in
+  let randl = jv_nf_betaiotaevar sigma randl in
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index db82c205c..96cafb072 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -156,7 +156,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = Context.Rel.map nf newps in
   let newfs = Context.Rel.map nf newfs in
-  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
+  let ce t = Pretyping.check_evars env0 Evd.empty evars t in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
     Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs