diff options
| author | letouzey | 2010-12-15 16:43:55 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-15 16:43:55 +0000 |
| commit | 2c2a1b91e994a4256d1bbebaa405ad114d834206 (patch) | |
| tree | 842a3af79fc808d2f381612d95f1bdc79b57c2c6 /plugins/syntax | |
| parent | 3c482becb02efe0a72e6363b6710094abdade86d (diff) | |
Clenv.connect_clenv without its Evd.fold
Apparently, it seems that clenv.evd is either created
from dummy_goal (in (e)auto) or from a copy of gls (in
class_tactics). I've checked experimentally by some assert
that on the stdlib the defined part of clenv.evd is always
included in gls. I hence propose to simplify this function
connect_clenv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13718 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions