From 7f2c52bcf588abfcbf30530bae240244229304a4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 27 Mar 2009 17:53:43 +0000 Subject: 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 --- theories/Strings/Ascii.v | 1 + theories/Strings/String.v | 1 + 2 files changed, 2 insertions(+) (limited to 'theories/Strings') diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 1f10f2aff..5a2cc9695 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 59edf8187..7d6696b78 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 *) -- cgit v1.2.3