diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-28 12:36:20 -0400 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-28 12:42:00 -0400 |
| commit | 0132b5b51fc1856356fb74130d3dea7fd378f76c (patch) | |
| tree | da5c0ec53dcecafb2fab5db1a112fac8b6311e60 /toplevel/vernacentries.ml | |
| parent | 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 (diff) | |
Univs: local names handling.
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2879947a9..31bfc004a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1527,7 +1527,7 @@ let vernac_check_may_eval redexp glopt rc = let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = @@ -1542,7 +1542,7 @@ let vernac_check_may_eval redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx uctx) + Printer.pr_universe_ctx sigma uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in |