From 5dd7a60ed62e01d6fb5310eac5b7adb33d6aced5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 9 Jun 2008 22:08:14 +0000 Subject: - Correction de la version simplifiée (filtrage sur deux sig imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml]. - Réactivation de l'interprétation des listes dans "generalize" cassée depuis 11072) [tacinterp.ml]. - Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_vernac.ml4 | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 33826c9f18..c128d7ae1e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -377,12 +377,10 @@ GEXTEND Gram | IDENT "End"; id = identref -> VernacEndSegment id (* Requiring an already compiled module *) - | IDENT "Require"; export = export_token; specif = specif_token; - qidl = LIST1 global -> - VernacRequire (export, specif, qidl) - | IDENT "Require"; export = export_token; specif = specif_token; - filename = ne_string -> - VernacRequireFrom (export, specif, filename) + | IDENT "Require"; export = export_token; qidl = LIST1 global -> + VernacRequire (export, None, qidl) + | IDENT "Require"; export = export_token; filename = ne_string -> + VernacRequireFrom (export, None, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr)) @@ -393,11 +391,6 @@ GEXTEND Gram | IDENT "Export" -> Some true | -> None ] ] ; - specif_token: - [ [ IDENT "Implementation" -> Some false - | IDENT "Specification" -> Some true - | -> None ] ] - ; of_module_type: [ [ ":"; mty = module_type -> (mty, true) | "<:"; mty = module_type -> (mty, false) ] ] -- cgit v1.2.3