aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorletouzey2010-12-15 16:43:44 +0000
committerletouzey2010-12-15 16:43:44 +0000
commit3c482becb02efe0a72e6363b6710094abdade86d (patch)
tree4832f1c5dfc3697c9af2b79716f21b5b5cd49a8f /plugins/syntax
parentd536aeb0c465b62c708ba4c70fd31b82c24168a5 (diff)
Evar-related speed-up and clarifications in Class_tactics and Rewrite
Some functions are restricted to consider only undefined evars, and some Evd.fold are replaced by Evd.fold_undefined. I'm less sure about the modifications in rewrite.ml4, but in pratice they seem to work well on the stdlib. I was planning to say assert false for Not_found in Rewrite.evd_of_existentials but some file of the stdlib doesn't like that (to be checked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions