diff options
| author | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
| commit | cfff8f8a32708ea0c8e72178424db0b40665fe37 (patch) | |
| tree | fe126ebb99be8e307df8a0a0f7837f51619a0eb8 /toplevel | |
| parent | bc8a5357889396f07d005a84bd3c50e9a25c1ddb (diff) | |
Experimental printing of the signature of open evars in Check.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |