Experimental printing of the signature of open evars in Check.

3 files changed, 12 insertions, 6 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index cba33929b9..33bd5041e8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -432,14 +432,15 @@ let pr_evar sigma (evk, evi) =
   hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
 
 (* Print an enumerated list of existential variables *)
-let rec pr_evars_int sigma i = function
+let rec pr_evars_int_hd head sigma i = function
   | [] -> mt ()
   | (evk,evi)::rest ->
-      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
-              pr_evar sigma (evk,evi))) ++
-      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int sigma (i+1) rest)
+      (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++
+      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest)
 
-let pr_evars_int sigma i evs = pr_evars_int sigma i (Evar.Map.bindings evs)
+let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs)
+
+let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
 
 let default_pr_subgoal n sigma =
   let rec prrec p = function
diff --git a/printing/printer.mli b/printing/printer.mli
index bac864dc6a..315bf6810d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -133,6 +133,7 @@ val pr_open_subgoals       : ?proof:Proof.proof -> unit -> std_ppcmds
 val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
+val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
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