diff options
| author | ppedrot | 2012-11-03 00:55:50 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-03 00:55:50 +0000 |
| commit | bcb8c0d7f0f5552fe302d0071d28c6d3c58ba7ab (patch) | |
| tree | 6f87a62791c50e93822418a135d649197a04230f /lib/xml_parser.ml | |
| parent | cf59f30fc9a4f5e90805b54a4c6d39c9bbd96e65 (diff) | |
Reversed roles of undefined/defined evars in Evd, thus saving precious
time when requesting only undefined evars (which is actually most often
the case, as in Goal.advance). Hopefully this should not disrupt anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15952 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions