diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 11:54:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 20:09:01 +0100 |
| commit | ef61bb05911d19c77d565d78dc57107d40c333e4 (patch) | |
| tree | be7f3694bbd0f5c6d31b931471a70059a9c4af3d | |
| parent | f4d77142a6e1d298fadf4219c46fcc9ff8abe62a (diff) | |
Isolate a function for printing evar sets.
| -rw-r--r-- | printing/printer.ml | 10 | ||||
| -rw-r--r-- | printing/printer.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
3 files changed, 14 insertions, 6 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 3403fb9c3..8a2d6e7bd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -446,6 +446,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) +(* Display a list of evars given by their name, with a prefix *) +let pr_ne_evar_set hd tl sigma l = + 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 + hd ++ pr_evars sigma l ++ tl + else + mt () + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." diff --git a/printing/printer.mli b/printing/printer.mli index 6b9c70815..42ed2b6d9 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -137,6 +137,8 @@ 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_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> + Evar.Set.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb12edfbc..bb2073001 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 |