diff options
| author | sacerdot | 2004-03-30 16:09:42 +0000 |
|---|---|---|
| committer | sacerdot | 2004-03-30 16:09:42 +0000 |
| commit | 45ed02f40b41c5e064d68a4bb364fd4bbe5cba07 (patch) | |
| tree | 47c646117a35ddd91941d5b11b7e86b1643ab70b /dev/base_include | |
| parent | 1fd9493d186f82e908412fbc3568f1f2358d8606 (diff) | |
The XML exportation hook for require is now active for:
- Require id.
- Require Export id.
- Require "file".
- Require Export "file".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5618 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions