From be0121602ff9fb3200cafead25e325617164038a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Oct 2014 11:07:48 +0200
Subject: Continuing experimental printing of the signature of open evars in
 Check (see cfff8f8a327) [printing only visible evars, not the ones
 corresponding to unrelated open goals + fixing bug on wrong sigma and on
 evar_info normalization].

---
 toplevel/vernacentries.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a41569377f..816912be40 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1481,16 +1481,20 @@ let vernac_check_may_eval redexp glopt rc =
   let c = nf c in
   let j =
     try
-      Evarutil.check_evars env Evd.empty sigma' c;
+      Evarutil.check_evars env sigma sigma' c;
       Arguments_renaming.rename_typing env c
     with Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) ->
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->
-        let l = Evarutil.non_instantiated sigma' in
-        let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma j.Environ.uj_type } in
+        let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
+        let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	msg_notice (print_judgment env sigma' j ++
-                    (if l != Evar.Map.empty then (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) else mt ()) ++
+                    (if l != Evar.Set.empty then
+                        let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in
+                        (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l)
+                     else
+                        mt ()) ++
                      Printer.pr_universe_ctx uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
-- 
cgit v1.2.3