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

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