From ccac2bd2f351088a5cd5966dba331817f51ac19e Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 parsing/extend.ml     | 47 -----------------------------------------------
 parsing/extend.mli    | 45 ---------------------------------------------
 parsing/parsing.mllib |  1 -
 parsing/ppvernac.ml   |  1 -
 4 files changed, 94 deletions(-)
 delete mode 100644 parsing/extend.ml
 delete mode 100644 parsing/extend.mli

(limited to 'parsing')

diff --git a/parsing/extend.ml b/parsing/extend.ml
deleted file mode 100644
index 22d640f50..000000000
--- 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 6b29fc747..000000000
--- 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 9adbb939a..d73e80f11 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 1f8d7cb83..b8782c67c 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