aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorppedrot2012-11-03 00:55:50 +0000
committerppedrot2012-11-03 00:55:50 +0000
commitbcb8c0d7f0f5552fe302d0071d28c6d3c58ba7ab (patch)
tree6f87a62791c50e93822418a135d649197a04230f /dev
parentcf59f30fc9a4f5e90805b54a4c6d39c9bbd96e65 (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 'dev')
0 files changed, 0 insertions, 0 deletions