diff options
| author | herbelin | 2008-04-15 12:00:50 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-15 12:00:50 +0000 |
| commit | 07e03e167c7eda30ffc989530470b5c597beaedc (patch) | |
| tree | 5bee610e35b3110430622cd1573d4971f70d28e4 /parsing | |
| parent | a036149469ef4c37e77018b1d47d24edfced6e04 (diff) | |
- Un peu de doc, préparation du CHANGES pour la release.
- Re-restriction de inversion (après la correction des bugs - et
notamment du "Unknown meta" qui apparaissait parfois -, inversion
devenait capable d'agir sur des buts non atomiques, ce qui crée
quelques incompatibilités, typiquement dans CoRN où inversion est
utilisé dans un rôle de discriminate; en attendant de voir, on
revient à la sémantique initiale).
- Généralisation de Local/Global dans Implicit Arguments pour avoir un
fonctionnement plus uniforme et plus facile à documenter.
- Code mort (clenv.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ae860d978d..45c16a1335 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -503,13 +503,10 @@ GEXTEND Gram (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ]; - (local,qid,pos) = - [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ]; - qid = global -> (local,qid,None) - | qid = global; - l = OPT [ "["; l = LIST0 implicit_name; "]" -> + local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; + qid = global; + pos = OPT [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - (true,qid,l) ] -> VernacDeclareImplicits (local,qid,enrich,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; |