diff options
| author | letouzey | 2011-11-04 17:44:41 +0000 |
|---|---|---|
| committer | letouzey | 2011-11-04 17:44:41 +0000 |
| commit | f06c30e82609e4d09fb2103a19ef501024251c6c (patch) | |
| tree | 0b77a88f39013269ee33526140882f5154f27e5b /plugins/syntax | |
| parent | 4b1656d0931209ac07660bebbf22d43d67581dee (diff) | |
Auto: removal of ?use_core_db obsolete now that we have nocore
Suggestion of Tom Prince, that told me that he has adapted the rippling
tactic to use the "nocore" pseudo-database. Since this tactic was the
only user of these optional arguments ?use_core_db, let's remove them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14629 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions