aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2009-12-14 19:05:05 +0000
committerherbelin2009-12-14 19:05:05 +0000
commitcc5c3eb26f817a0a1cd479c0f7f3083e648b9a9b (patch)
treed5de785d0560bb7c867560e8b09408b7f24a117e /dev
parentf698148f6aee01a207ce5ddd4bebf19da2108bff (diff)
Improved strategy for rewriting lemma possibly depending because of evars.
Explained in CHANGES how to cope with the change of semantics of abbreviations wrt implicit arguments positions propagation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions