diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 3 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/BigNumPrelude.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 1 | ||||
| -rw-r--r-- | theories/Strings/Ascii.v | 1 | ||||
| -rw-r--r-- | theories/Strings/String.v | 1 |
7 files changed, 11 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". diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 209eb5497f..076bceba48 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -10,6 +10,8 @@ Unset Boxed Definitions. +Declare ML Module "z_syntax_plugin". + (**********************************************************************) (** Binary positive numbers *) diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 633cc84230..d890d9287b 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -21,6 +21,8 @@ Require Export ZArith. Require Export Znumtheory. Require Export Zpow_facts. +Declare ML Module "numbers_syntax_plugin". + (* *** Nota Bene *** All results that were general enough has been moved in ZArith. Only remain here specialized lemmas and compatibility elements. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 63b8928fb2..897d5c7100 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,6 +12,7 @@ (** Definitions for the axiomatization *) (*********************************************************) +Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 1f10f2affd..5a2cc96957 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,6 +13,7 @@ Require Import Bool. Require Import BinPos. +Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 59edf81871..7d6696b782 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -13,6 +13,7 @@ Require Import Arith. Require Import Ascii. +Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) |