diff options
| author | msozeau | 2009-09-02 20:43:25 +0000 |
|---|---|---|
| committer | msozeau | 2009-09-02 20:43:25 +0000 |
| commit | 07bd9c28f37b9ec390e5e3dcacdfd8183056be88 (patch) | |
| tree | 4f5fc9a2e58e2da676db4ec3f2a64806f9233016 /plugins/setoid_ring | |
| parent | c7254961b3a851fc5412e1db88a24a13b43773a7 (diff) | |
Hack to correctly get ill-formed rec body exceptions even
when the environment is reset. Bug is due to the use of
the imperative the_globrevtab when trying to pretty-print the terms
involved which may refer to the last defined obligation which is defined
in the exception's environment and not the global one anymore.
Bug reported by Francois Pottier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring')
0 files changed, 0 insertions, 0 deletions