From 1f95f087d79d6c2c79012921ce68553caf20b090 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 5 Nov 2002 16:59:16 +0000 Subject: Intégration des modifs de la branche mowgli : - Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pcoq.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'parsing/pcoq.ml4') diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d72a06f2a..67322863a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -13,7 +13,6 @@ open Util open Ast open Genarg open Tacexpr -open Vernacexpr (* The lexer of Coq *) @@ -75,6 +74,7 @@ type typed_entry = entry_type Gramobj.entry module type Gramtypes = sig + open Decl_kinds val inAstListType : Coqast.t list G.Entry.e -> typed_entry val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry -- cgit v1.2.3