diff options
| author | Pierre-Marie Pédrot | 2014-09-19 19:14:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-19 19:14:04 +0200 |
| commit | 6473b8d6df7a9b95410a6c4a5d85012d8e33ba82 (patch) | |
| tree | b8e056b0b87ce3f9472b7e70407127cf580e395f | |
| parent | b704074e906cfd7aff1b4f02e17b7919b20e8a7d (diff) | |
Fixing bug #3646.
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 10b1f48c3a..7962e52bad 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -703,7 +703,7 @@ let pr_constraints printenv env sigma evars cstrs = let evs = prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr 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 |