diff options
| author | Pierre-Marie Pédrot | 2015-01-25 18:05:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-25 18:05:42 +0100 |
| commit | 8434840413d7cef32ed83539a0c7ef4de13ec528 (patch) | |
| tree | b6ea2152ef16ce0953b889b2c2ad93c364e61e19 /toplevel | |
| parent | 4e515c483e41f0362bf1102f8e8ae071fdcf04f7 (diff) | |
| parent | 3d6b9a7ab992559493b89e174549734dff401703 (diff) | |
Merge branch 'v8.5' into trunk.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
2 files changed, 3 insertions, 7 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e6b2382867..fbc45b4ae3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -85,7 +85,7 @@ let _ = { optsync = true; optdepr = false; optname = "automatic declaration of boolean equality"; - optkey = ["Equality";"Schemes"]; + optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb12edfbc2..bb20730015 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1516,12 +1516,8 @@ let vernac_check_may_eval redexp glopt rc = let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) 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.Set.empty then - let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in - (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) - else - mt ()) ++ - Printer.pr_universe_ctx uctx) + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in |