updated printing of evar context (may loop ?)

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

8 files changed, 27 insertions, 16 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3004f39e96..8142664683 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -359,7 +359,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
        in
         (* We map the named context to a rel context and every Var to a Rel *)
         (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
-   ) (Evd.non_instantiated evar_map)
+   ) (Evarutil.non_instantiated evar_map)
  in
   let id' = Names.string_of_id id in
    if metasenv = [] then
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index bd65b6ab27..1ccf8f5230 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -83,6 +83,15 @@ let jl_nf_evar = Pretype_errors.jl_nf_evar
 let jv_nf_evar = Pretype_errors.jv_nf_evar
 let tj_nf_evar = Pretype_errors.tj_nf_evar
 
+let nf_evar_info evc info =
+  { evar_concl = Reductionops.nf_evar evc info.evar_concl;
+    evar_hyps = List.map 
+		  (fun (id,body,typ) -> 
+		     (id,
+		      option_app (Reductionops.nf_evar evc) body,
+		      Reductionops.nf_evar evc typ)) info.evar_hyps; 
+    evar_body = info.evar_body}
+
 (**********************)
 (* Creating new evars *)
 (**********************)
@@ -236,8 +245,6 @@ let ise_try isevars l =
        or (isevars.evars <- u; test l)
   in test l
 
-
-
 (* say if the section path sp corresponds to an existential *)
 let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp
 
@@ -258,6 +265,15 @@ let ise_undefined isevars c = match kind_of_term c with
 
 let need_restriction isevars args = not (array_for_all closed0 args)
     
+(* The list of non-instantiated existential declarations *)
+
+let non_instantiated sigma = 
+  let listev = to_list sigma in
+  List.fold_left 
+    (fun l (ev,evd) -> 
+       if evd.evar_body = Evar_empty then 
+	 ((ev,nf_evar_info sigma evd)::l) else l)
+    [] listev
 
 (* We try to instanciate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times.
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 812f3e9342..5e534f59cd 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -32,6 +32,8 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
+val nf_evar_info : evar_map -> evar_info -> evar_info
+
 (* Replacing all evars *)
 exception Uninstantiated_evar of existential_key
 val whd_ise :  evar_map -> constr -> constr
@@ -45,6 +47,9 @@ val evar_env :  evar_info -> env
 
 type evar_defs
 val evars_of :  evar_defs ->  evar_map
+
+val non_instantiated : evar_map -> (evar * evar_info) list
+
 val create_evar_defs :  evar_map ->  evar_defs
 val evars_reset_evd :  evar_map ->  evar_defs -> unit
 val evar_source : existential_key -> evar_defs -> loc * hole_kind
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 66ec64ea16..094689d45e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -51,15 +51,6 @@ let define evd ev body =
   match oldinfo.evar_body with
     | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
-
-(* The list of non-instantiated existential declarations *)
-
-let non_instantiated sigma = 
-  let listev = to_list sigma in
-  List.fold_left 
-    (fun l ((ev,evd) as d) -> 
-       if evd.evar_body = Evar_empty then (d::l) else l)
-    [] listev
     
 let is_evar sigma ev = in_dom sigma ev
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2ad83c16a7..0ea82da7c5 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -46,7 +46,6 @@ val to_list : evar_map -> (evar * evar_info) list
 
 val define : evar_map -> evar -> constr -> evar_map
 
-val non_instantiated : evar_map -> (evar * evar_info) list
 val is_evar : evar_map -> evar -> bool
 
 val is_defined : evar_map -> evar -> bool
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b04691d87b..719d95aedc 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -153,7 +153,7 @@ let instantiate_pf_com n com pfts =
   let sigma = (w_Underlying wc) in 
   let (sp,evd) (* as evc *) = 
     try
-      List.nth (Evd.non_instantiated sigma) (n-1) 
+      List.nth (Evarutil.non_instantiated sigma) (n-1) 
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 6358b71892..271592b73a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -229,7 +229,7 @@ let rec pr_evars_int i = function
 
 let pr_subgoals_existential sigma = function 
   | [] -> 
-      let exl = Evd.non_instantiated sigma in 
+      let exl = non_instantiated sigma in 
       if exl = [] then 
 	(str"Proof completed."  ++ fnl ())
       else
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7c19954542..ace6416dc2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -98,7 +98,7 @@ let show_top_evars () =
   let pfts = get_pftreestate () in 
   let gls = top_goal_of_pftreestate pfts in 
   let sigma = project gls in 
-  msg (pr_evars_int 1 (Evd.non_instantiated sigma))
+  msg (pr_evars_int 1 (Evarutil.non_instantiated sigma))
 
 let show_prooftree () =
   let pts = get_pftreestate () in