5 files changed, 14 insertions, 14 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 29ce9d3d4a..491b44fbba 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1894,7 +1894,7 @@ let liftn_rel_context n k sign =
     liftrec (k + rel_context_length sign) sign
 
 let nf_evars_env sigma (env : env) : env =
-  let nf t = nf_isevar sigma t in
+  let nf t = nf_evar sigma t in
   let env0 : env = reset_context env in
   let f e (na, b, t) e' : env =
     Environ.push_named (na, Option.map nf b, nf t) e'
@@ -1912,7 +1912,7 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon
     match rtntyp with
       | Some rtntyp ->
 	  let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
-	  let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+	  let predccl = (j_nf_evar !isevars predcclj).uj_val in
 	    Some (build_initial_predicate true allnames predccl)
       | None ->
 	  match valcon_of_tycon tycon with
@@ -1993,7 +1993,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
 	let j =
 	  { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
-	    uj_type = nf_isevar !isevars tycon; }
+	    uj_type = nf_evar !isevars tycon; }
 	in j
     else
       (* We build the elimination predicate if any and check its consistency *)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 4a254d7910..2fe22364d5 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -164,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	let term = Termops.it_mkLambda_or_LetIn def ctx in
 	  term, termtype
   in
-  let termtype = Evarutil.nf_isevar !evars termtype in
-  let term = Evarutil.nf_isevar !evars term in
+  let termtype = Evarutil.nf_evar !evars termtype in
+  let term = Evarutil.nf_evar !evars term in
   evars := undefined_evars !evars;
   Evarutil.check_evars env Evd.empty !evars termtype;
   let hook vis gr =
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 1bc3dbb345..3c907962ce 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -456,8 +456,8 @@ module Coercion = struct
 	  let (evd', val') =
 	    try
 	      inh_conv_coerce_to_fail loc env evd rigidonly
-		(Some (nf_isevar evd cj.uj_val))
-		(nf_isevar evd cj.uj_type) (nf_isevar evd t)
+		(Some (nf_evar evd cj.uj_val))
+		(nf_evar evd cj.uj_type) (nf_evar evd t)
 	    with NoCoercion ->
 	      let sigma =  evd in
 		try
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 8a7d11d1d8..d93a4b695e 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -50,7 +50,7 @@ open Subtac_obligations
 (* Functions to parse and interpret constructions *)
 
 let evar_nf isevars c =
-  Evarutil.nf_isevar !isevars c
+  Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
@@ -213,7 +213,7 @@ let telescope = function
 
 let nf_evar_context isevars ctx =
   List.map (fun (n, b, t) ->
-    (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+    (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
 
 let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
@@ -318,7 +318,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let _ = isevars := Evarutil.nf_evar_map !isevars in
   let binders_rel = nf_evar_context !isevars binders_rel in
   let binders = nf_evar_context !isevars binders in
-  let top_arity = Evarutil.nf_isevar !isevars top_arity in
+  let top_arity = Evarutil.nf_evar !isevars top_arity in
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -326,7 +326,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ce =
-	  { const_entry_body = Evarutil.nf_isevar !isevars body;
+	  { const_entry_body = Evarutil.nf_evar !isevars body;
 	    const_entry_type = Some ty;
 	    const_entry_opaque = false;
 	    const_entry_boxed = false} 
@@ -345,8 +345,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	  Impargs.declare_manual_implicits false gr impls
       in hook, recname, typ
   in
-  let fullcoqc = Evarutil.nf_isevar !isevars def in
-  let fullctyp = Evarutil.nf_isevar !isevars typ in
+  let fullcoqc = Evarutil.nf_evar !isevars def in
+  let fullctyp = Evarutil.nf_evar !isevars typ in
   let evm = evars_of_term !isevars Evd.empty fullctyp in
   let evm = evars_of_term !isevars evm fullcoqc in
   let evm = non_instanciated_map env isevars evm in
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index a59cb96652..5b42c8ba5f 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -125,7 +125,7 @@ let subtac_process env isevars id bl c tycon =
   let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars !isevars in
-  let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+  let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
     evm, coqc, ty, imps
 
 open Subtac_obligations