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, 51 insertions, 62 deletions

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