diff options
| author | Matthieu Sozeau | 2014-10-08 23:28:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-10 20:40:04 +0200 |
| commit | 8a9de08c0e6a5130103cedf05cbcebcf5f621d1e (patch) | |
| tree | 8dd91ad2d43fb99cb99115c5b5377f4a142f8947 /toplevel | |
| parent | 32653d69478992d55dc45a5562aeb6b41ae67f21 (diff) | |
Add debug printers for projections, fix printing of evar constraints
and unsatisfiable constraints which were not done in the right environment.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 90df174279..37205e404d 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 |