From ccac2bd2f351088a5cd5966dba331817f51ac19e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:30 +0000
Subject: Extend become a mli-only file in intf/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15390 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib    |  1 -
 grammar/grammar.mllib |  1 -
 intf/extend.mli       | 45 +++++++++++++++++++++++++++++++++++++++++++++
 parsing/extend.ml     | 47 -----------------------------------------------
 parsing/extend.mli    | 45 ---------------------------------------------
 parsing/parsing.mllib |  1 -
 parsing/ppvernac.ml   |  1 -
 7 files changed, 45 insertions(+), 96 deletions(-)
 create mode 100644 intf/extend.mli
 delete mode 100644 parsing/extend.ml
 delete mode 100644 parsing/extend.mli

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 928bfc4940..03d62e2074 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -132,7 +132,6 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
-Extend
 Extrawit
 Pcoq
 Printer
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 195ad38c02..5ab3057fed 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -18,7 +18,6 @@ Libnames
 Genarg
 Tok
 Lexer
-Extend
 Extrawit
 Pcoq
 Q_util
diff --git a/intf/extend.mli b/intf/extend.mli
new file mode 100644
index 0000000000..6b29fc7476
--- /dev/null
+++ b/intf/extend.mli
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Compat
+
+(** Entry keys for constr notations *)
+
+type side = Left | Right
+
+type production_position =
+  | BorderProd of side * gram_assoc option
+  | InternalProd
+
+type production_level =
+  | NextLevel
+  | NumLevel of int
+
+type ('lev,'pos) constr_entry_key_gen =
+  | ETName | ETReference | ETBigint
+  | ETBinder of bool
+  | ETConstr of ('lev * 'pos)
+  | ETPattern
+  | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
+
+(** Entries level (left-hand-side of grammar rules) *)
+
+type constr_entry_key =
+    (int,unit) constr_entry_key_gen
+
+(** Entries used in productions (in right-hand-side of grammar rules) *)
+
+type constr_prod_entry_key =
+    (production_level,production_position) constr_entry_key_gen
+
+(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+
+type simple_constr_prod_entry_key =
+    (production_level,unit) constr_entry_key_gen
diff --git a/parsing/extend.ml b/parsing/extend.ml
deleted file mode 100644
index 22d640f508..0000000000
--- a/parsing/extend.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Compat
-open Errors
-open Util
-
-(** Entry keys for constr notations *)
-
-type side = Left | Right
-
-type production_position =
-  | BorderProd of side * gram_assoc option
-  | InternalProd
-
-type production_level =
-  | NextLevel
-  | NumLevel of int
-
-type ('lev,'pos) constr_entry_key_gen =
-  | ETName | ETReference | ETBigint
-  | ETBinder of bool (* true=open, as in "fun .."; false as in "let f .. :=" *)
-  | ETConstr of ('lev * 'pos)
-  | ETPattern
-  | ETOther of string * string
-  | ETConstrList of ('lev * 'pos) * Tok.t list
-  | ETBinderList of bool * Tok.t list
-
-(**  Entries level (left-hand-side of grammar rules) *)
-
-type constr_entry_key =
-    (int,unit) constr_entry_key_gen
-
-(** Entries used in productions (in right-hand side of grammar rules) *)
-
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
-
-(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
-
-type simple_constr_prod_entry_key =
-    (production_level,unit) constr_entry_key_gen
diff --git a/parsing/extend.mli b/parsing/extend.mli
deleted file mode 100644
index 6b29fc7476..0000000000
--- a/parsing/extend.mli
+++ /dev/null
@@ -1,45 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Compat
-
-(** Entry keys for constr notations *)
-
-type side = Left | Right
-
-type production_position =
-  | BorderProd of side * gram_assoc option
-  | InternalProd
-
-type production_level =
-  | NextLevel
-  | NumLevel of int
-
-type ('lev,'pos) constr_entry_key_gen =
-  | ETName | ETReference | ETBigint
-  | ETBinder of bool
-  | ETConstr of ('lev * 'pos)
-  | ETPattern
-  | ETOther of string * string
-  | ETConstrList of ('lev * 'pos) * Tok.t list
-  | ETBinderList of bool * Tok.t list
-
-(** Entries level (left-hand-side of grammar rules) *)
-
-type constr_entry_key =
-    (int,unit) constr_entry_key_gen
-
-(** Entries used in productions (in right-hand-side of grammar rules) *)
-
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
-
-(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
-
-type simple_constr_prod_entry_key =
-    (production_level,unit) constr_entry_key_gen
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 9adbb939a9..d73e80f113 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,5 @@
 Tok
 Lexer
-Extend
 Extrawit
 Pcoq
 Egramml
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1f8d7cb83b..b8782c67c3 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -19,7 +19,6 @@ open Ppconstr
 open Pptactic
 open Glob_term
 open Genarg
-open Pcoq
 open Libnames
 open Ppextend
 open Constrexpr
-- 
cgit v1.2.3