From cfff8f8a32708ea0c8e72178424db0b40665fe37 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Oct 2014 15:14:54 +0200
Subject: Experimental printing of the signature of open evars in Check.

---
 toplevel/vernacentries.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8107fc06f4..a41569377f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1487,7 +1487,11 @@ let vernac_check_may_eval redexp glopt rc =
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->
-	msg_notice (print_judgment env sigma' j ++ Printer.pr_universe_ctx uctx)
+        let l = Evarutil.non_instantiated sigma' 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 ()) ++
+                     Printer.pr_universe_ctx uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
-- 
cgit v1.2.3