diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-08 23:28:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-10 20:40:04 +0200 |
| commit | 8a9de08c0e6a5130103cedf05cbcebcf5f621d1e (patch) | |
| tree | 8dd91ad2d43fb99cb99115c5b5377f4a142f8947 | |
| parent | 32653d69478992d55dc45a5562aeb6b41ae67f21 (diff) | |
Add debug printers for projections, fix printing of evar constraints
and unsatisfiable constraints which were not done in the right environment.
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 5 | ||||
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 5 |
4 files changed, 9 insertions, 6 deletions
diff --git a/dev/base_include b/dev/base_include index 1d43e64df..c2da8b18a 100644 --- a/dev/base_include +++ b/dev/base_include @@ -34,6 +34,7 @@ #install_printer (* qualid *) ppqualid;; #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; +#install_printer (* projection *) ppproj;; #install_printer (* cl_index *) ppclindex;; #install_printer (* recarg Rtree.t *) ppwf_paths;; #install_printer (* constr *) print_pure_constr;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 1d903f30f..75310163f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -43,6 +43,7 @@ let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (string_of_mp mp)) let ppcon con = pp(debug_pr_con con) +let ppproj con = pp(debug_pr_con (Projection.constant con)) let ppkn kn = pp(pr_kn kn) let ppmind kn = pp(debug_pr_mind kn) let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i) @@ -146,8 +147,8 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map (Some 2) evd) -let ppevmall evd = pp(pr_evar_map None evd) +let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) +let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 822a3cb7c..028361185 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1777,11 +1777,11 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr t1 ++ spc () ++ + print_constr_env env t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr t2 + spc () ++ print_constr_env env t2 in prlist_with_sep fnl pr_evconstr pbs diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 90df17427..37205e404 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -696,16 +696,17 @@ let pr_constraints printenv env sigma evars cstrs = eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars then let l = Evar.Map.bindings evars in + let env' = reset_with_named_context evi.evar_hyps env in let pe = if printenv then pr_ne_context_of (str "In environment:") (mt ()) - (reset_with_named_context evi.evar_hyps env) sigma ++ fnl () + env' sigma ++ fnl () else mt () in let evs = prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env sigma evi.evar_concl) l + str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l in pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs) else |