diff options
| author | Gaëtan Gilbert | 2018-08-22 16:40:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-28 12:50:05 +0200 |
| commit | 3aa3c4590ce7d32657cd48ea021254e4215e2889 (patch) | |
| tree | 20277ef9a5de475c8eb2f48e55a62b7feebeef77 /vernac | |
| parent | a7b09ef087d82e0b733356e6f22dd5a79b967788 (diff) | |
Close #8091: print universe context for Eval when option on.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e1228e9d78..41586eed8b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1706,14 +1706,13 @@ let vernac_check_may_eval ~atts redexp glopt rc = (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in - match redexp with + let pp = match redexp with | None -> let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in print_judgment env sigma j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l ++ - Printer.pr_universe_ctx_set sigma uctx + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l | Some r -> let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in let redfun env evm c = @@ -1722,6 +1721,8 @@ let vernac_check_may_eval ~atts redexp glopt rc = c in print_eval redfun env sigma rc j + in + pp ++ Printer.pr_universe_ctx_set sigma uctx let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in |