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

4 files changed, 23 insertions, 12 deletions

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