diff options
| author | herbelin | 2008-06-09 22:08:14 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-09 22:08:14 +0000 |
| commit | 5dd7a60ed62e01d6fb5310eac5b7adb33d6aced5 (patch) | |
| tree | 04d6574085dd26490282d7c82a70ccbfabd75710 /parsing | |
| parent | 7d2ac586a0f7dc0a497d1c94a9320a11c3e1f3c5 (diff) | |
- 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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 15 |
1 files changed, 4 insertions, 11 deletions
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) ] ] |