diff options
| author | letouzey | 2009-03-27 17:53:43 +0000 |
|---|---|---|
| committer | letouzey | 2009-03-27 17:53:43 +0000 |
| commit | 7f2c52bcf588abfcbf30530bae240244229304a4 (patch) | |
| tree | 6a74c2b13c24e66076177d51e188724c06ef0720 /theories/Init | |
| parent | 999ac2c4c2bb6c7397c88ee1b6f39bdb43eaecb1 (diff) | |
Parsing files for numerals (+ ascii/string) moved into plugins
Idea: make coqtop more independant of the standard library.
In the future, we can imagine loading the syntax for numerals right
after their definition. For the moment, it is easier to stay lazy
and load the syntax plugins slightly before the definitions.
After this commit, the main (sole ?) references to theories/
from the core ml files are in Coqlib (but many parts of coqlib
are only used by plugins), and it mainly concerns Init
(+ Logic/JMeq and maybe a few others).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 73e4924aaa..2194b93a3f 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,6 +12,8 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. +Declare ML Module "nat_syntax_plugin". + (** [unit] is a singleton datatype with sole inhabitant [tt] *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 84de55e24d..685c724703 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,7 +15,8 @@ Require Export Specif. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. -(* Initially available plugins *) +(* Initially available plugins + (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". |