diff options
| author | Hugo Herbelin | 2020-05-10 22:54:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 12:21:30 +0200 |
| commit | cd1bb55339040bc272a9a752703e259e27ddbcd4 (patch) | |
| tree | d7628e94b5364ee9678b5b6ba1793450e5e613cc /pretyping/pretype_errors.mli | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Fixes #12234 (wrong environment for Show Proof).
We take the env of the current goal with the context replaced with
section variables. In practice, this is the global env, but, maybe,
one day, a goal state will have its own env.
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions