Made tclABSTRACT normalize evars before saying it does not support

them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).

Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.

Removed obsolete printer mod_self_id from dev/db.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 94 insertions, 92 deletions

diff --git a/dev/db b/dev/db
index ca5c27de3b..6be2c20b92 100644
--- a/dev/db
+++ b/dev/db
@@ -6,8 +6,6 @@ install_printer Top_printers.ppidset
 install_printer Top_printers.ppevarsubst
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
-install_printer Top_printers.ppmsid
-install_printer Top_printers.ppmbid
 install_printer Top_printers.ppdir
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 784283358a..1321b49785 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -17,6 +17,11 @@ generally fewer than the defined ones.
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Light cleaning in evarutil.ml **
+
+whd_castappevar is now whd_head_evar
+obsolete whd_ise disappears
+
 ** Semantical change of h_induction_destruct **
 
 Warning, the order of the isrec and evar_flag was inconsistent and has
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
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa0f4843fa..da417f44df 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1655,7 +1655,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 	  evdref :=
             Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
         tycon;
-      let predccl = (j_nf_isevar !evdref predcclj).uj_val in
+      let predccl = (j_nf_evar !evdref predcclj).uj_val in
       [!evdref, KnownDep, predccl]
   in
   List.map
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 486fd05b3d..3a236671ab 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -159,8 +159,8 @@ let ise_array2 evd f v1 v2 =
 
 let rec evar_conv_x env evd pbty term1 term2 =
   let sigma =  evd in
-  let term1 = whd_castappevar sigma term1 in
-  let term2 = whd_castappevar sigma term2 in
+  let term1 = whd_head_evar sigma term1 in
+  let term2 = whd_head_evar sigma term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
@@ -187,7 +187,7 @@ let rec evar_conv_x env evd pbty term1 term2 =
             (decompose_app term1) (decompose_app term2)
 
 and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
-  (* Evar must be undefined since we have whd_ised *)
+  (* Evar must be undefined since we have flushed evars *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
@@ -521,8 +521,8 @@ let choose_less_dependent_instance evk evd term args =
   Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_castappevar evd t1) in
-  let t2 = apprec_nohdbeta env evd (whd_castappevar evd t2) in
+  let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
+  let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e104fe9083..c7258ccfeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,33 +21,18 @@ open Reductionops
 open Pretype_errors
 open Retyping
 
-(* Expanding existential variables (pretyping.ml) *)
-(* 1- whd_ise fails if an existential is undefined *)
+(* Expanding existential variables *)
+(* 1- flush_and_check_evars fails if an existential is undefined *)
 
 exception Uninstantiated_evar of existential_key
 
-let rec whd_ise sigma c =
+let rec flush_and_check_evars sigma c =
   match kind_of_term c with
-  | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
-      whd_ise sigma (existential_value sigma ev)
-  | Evar (evk,_) when Evd.is_undefined sigma evk ->
-      raise (Uninstantiated_evar evk)
-  | _ -> c
-
-
-(* Expand evars, possibly in the head of an application *)
-let whd_castappevar_stack sigma c =
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | Evar (evk,args as ev) when Evd.is_defined sigma evk
-	  -> whrec (existential_value sigma ev, l)
-      | Cast (c,_,_) -> whrec (c, l)
-      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
-      | _ -> s
-  in
-  whrec (c, [])
-
-let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
+  | Evar (evk,_ as ev) ->
+      (match existential_opt_value sigma ev with
+       | None -> raise (Uninstantiated_evar evk)
+       | Some c -> flush_and_check_evars sigma c)
+  | _ -> map_constr (flush_and_check_evars sigma) c
 
 let nf_evar = Pretype_errors.nf_evar
 let j_nf_evar = Pretype_errors.j_nf_evar
@@ -79,12 +64,6 @@ let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info ev
 
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 
-let nf_isevar evd = nf_evar evd
-let j_nf_isevar evd = j_nf_evar evd
-let jl_nf_isevar evd = jl_nf_evar evd
-let jv_nf_isevar evd = jv_nf_evar evd
-let tj_nf_isevar evd = tj_nf_evar evd
-
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -1177,6 +1156,8 @@ let is_ground_env evd env =
    structures *)
 let is_ground_env = memo1_2 is_ground_env
 
+(* Return the head evar if any *)
+
 exception NoHeadEvar
 
 let head_evar =
@@ -1189,6 +1170,22 @@ let head_evar =
   in
   hrec
 
+(* Expand head evar if any (currently consider only applications but I
+   guess it should consider Case too) *)
+
+let whd_head_evar_stack sigma c =
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | Evar (evk,args as ev) when Evd.is_defined sigma evk
+	  -> whrec (existential_value sigma ev, l)
+      | Cast (c,_,_) -> whrec (c, l)
+      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | _ -> s
+  in
+  whrec (c, [])
+
+let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
+
 (* Check if an applied evar "?X[args] l" is a Miller's pattern; note
    that we don't care whether args itself contains Rel's or even Rel's
    distinct from the ones in l *)
@@ -1338,10 +1335,10 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 	  let evi = Evd.find evd evk1 in
 	    if occur_existential evd evi.evar_concl then
 	      let evenv = evar_unfiltered_env evi in
-	      let evc = nf_isevar evd evi.evar_concl in
+	      let evc = nf_evar evd evi.evar_concl in
 		match evi.evar_body with
 		| Evar_defined body ->
-		    let ty = nf_isevar evd (Retyping.get_type_of evenv evd body) in
+		    let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
 		      add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
 		| Evar_empty -> (* Resulted in a constraint *)
 		    evd
@@ -1379,18 +1376,17 @@ let evars_of_evar_info evi =
 	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
 
 (* [check_evars] fails if some unresolved evar remains *)
-(* it assumes that the defined existentials have already been substituted *)
 
-let check_evars env initial_sigma evd c =
-  let sigma =  evd in
-  let c = nf_evar sigma c in
+let check_evars env initial_sigma sigma c =
   let rec proc_rec c =
     match kind_of_term c with
-      | Evar (evk,args) ->
-          assert (Evd.mem sigma evk);
+    | Evar (evk,_ as ev) ->
+        (match existential_opt_value sigma ev with
+        | Some c -> proc_rec c
+        | None -> 
 	  if not (Evd.mem initial_sigma evk) then
-            let (loc,k) = evar_source evk evd in
-	      (match k with
+            let (loc,k) = evar_source evk sigma in
+	      match k with
 	      | ImplicitArg (gr, (i, id), false) -> ()
 	      | _ ->
 		  let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 1d11097d30..e47d452b00 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -69,9 +69,13 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 (**********************************************************
    Unification utils *)
 
+(** [head_evar c} returns the head evar of [c] if any *)
 exception NoHeadEvar
 val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
 
+(* Expand head evar if any *)
+val whd_head_evar :  evar_map -> constr -> constr
+
 val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 val solve_refl :
@@ -132,8 +136,8 @@ val lift_tycon : int -> type_constraint -> type_constraint
 
 (***********************************************************)
 
-(** [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; 
-   *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
+(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
+    uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
 val nf_evar :  evar_map -> constr -> constr
 val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
@@ -151,22 +155,11 @@ val nf_named_context_evar : evar_map -> named_context -> named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
-(** Same for evar defs *)
-val nf_isevar :  evar_map -> constr -> constr
-val j_nf_isevar :  evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_isevar :
-   evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_isevar :
-   evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_isevar :
-   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
 val nf_evar_map : evar_map -> evar_map
 
-(** Replacing all evars *)
+(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
-val whd_ise :  evar_map -> constr -> constr
-val whd_castappevar :  evar_map -> constr -> constr
+val flush_and_check_evars :  evar_map -> constr -> constr
 
 (** Replace the vars and rels that are aliases to other vars and rels by 
    their representative that is most ancient in the context *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 411dc0da6a..a2a37edfc8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -221,8 +221,8 @@ let oracle_order env cf1 cf2 =
 
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
-    let cM = Evarutil.whd_castappevar sigma curm
-    and cN = Evarutil.whd_castappevar sigma curn in
+    let cM = Evarutil.whd_head_evar sigma curm
+    and cN = Evarutil.whd_head_evar sigma curn in
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
 	    let stM,stN = extract_instance_status pb in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 12a14eb014..a0d0027e42 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1006,12 +1006,12 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	    let cstrevars = !evars in
 	    let evars = solve_constraints env cstrevars in
 	    let p = map_rewprf 
-	      (fun p -> nf_zeta env evars (Evarutil.nf_isevar evars p)) 
+	      (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) 
 	      p 
 	    in
-	    let newt = Evarutil.nf_isevar evars newt in
+	    let newt = Evarutil.nf_evar evars newt in
 	    let abs = Option.map (fun (x, y) ->
-	      Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in
+	      Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in
 	    let undef = split_evars (fst cstrevars) evars in
 	    let rewtac =
 	      match is_hyp with
@@ -1422,7 +1422,7 @@ let build_morphism_signature m =
     mkApp (Lazy.force proper_type, [| t; sig_; m |])
   in
   let evd = solve_constraints env !isevars in
-  let m = Evarutil.nf_isevar evd morph in
+  let m = Evarutil.nf_evar evd morph in
     Evarutil.check_evars env Evd.empty evd m; m
 
 let default_morphism sign m =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0be1e08fc6..9f5c611234 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2470,7 +2470,7 @@ let specialize_eqs id gl =
   let acc' = it_mkLambda_or_LetIn acc ctx'' in
   let ty' = Tacred.whd_simpl env !evars ty' 
   and acc' = Tacred.whd_simpl env !evars acc' in
-  let ty' = Evarutil.nf_isevar !evars ty' in
+  let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(exact_no_check (refresh_universes_strict acc')) gl
@@ -3463,8 +3463,10 @@ let abstract_subproof id tac gl =
       global_sign (empty_named_context,empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
-  if occur_existential concl then
-    error "\"abstract\" cannot handle existentials.";
+  let concl =
+    try flush_and_check_evars (project gl) concl
+    with Uninstantiated_evar _ ->
+      error "\"abstract\" cannot handle existentials." in
   let const = Pfedit.build_constant_by_tactic secsign concl
     (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
index 6acdd51616..0b112937e5 100644
--- a/test-suite/success/replace.v
+++ b/test-suite/success/replace.v
@@ -22,3 +22,11 @@ replace x with 0 in H,H0 |- * .
 Undo.
 Admitted.
 
+(* This failed at some point when "replace" started to support arguments
+   with evars but "abstract" did not supported any evars even defined ones *)
+
+Class U.
+Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0.
+replace (f _) with 0 by abstract apply H.
+reflexivity.
+Qed.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d161470245..62a7ebb445 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -184,7 +184,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	    Evarutil.nf_isevar !evars t
+	    Evarutil.nf_evar !evars t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_internal_constant id
@@ -249,8 +249,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	      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
 	let evm = undefined_evars !evars in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	  if Evd.is_empty evm then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8d840a4580..4259ccb81c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -73,7 +73,7 @@ let interp_definition boxed bl red_option c ctypopt =
     match ctypopt with
       None ->
 	let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in
-	let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
+	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	check_evars env Evd.empty !evdref body;
 	imps1@imps2,
 	{ const_entry_body = body;
@@ -83,8 +83,8 @@ let interp_definition boxed bl red_option c ctypopt =
     | Some ctyp ->
 	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
 	let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
-	let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
-	let typ = nf_isevar !evdref (it_mkProd_or_LetIn ty ctx) in
+	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
+	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
 	check_evars env Evd.empty !evdref body;
 	check_evars env Evd.empty !evdref typ;
 	imps1@imps2,
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 01cfd22e81..efb0595ab6 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -320,7 +320,7 @@ let start_proof_com kind thms hook =
     Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
     let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
-      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
+      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
     thms in