diff options
| author | msozeau | 2009-12-27 22:08:57 +0000 |
|---|---|---|
| committer | msozeau | 2009-12-27 22:08:57 +0000 |
| commit | 42ea537affb88f8e63499d909eb526e024fc0aec (patch) | |
| tree | 15d95ea521cd5b5ee592cee7c818cf45b413debf /parsing | |
| parent | fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa (diff) | |
Fix "Existing Instance" to handle globality information and "Existing
Class" too to handle references instead of just idents. Minor fix in
coqdoc. zeta-normalize setoid_rewrite proofs, removing useless
let-bindings generated by the tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 7 |
2 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cb7507d9c1..3baed8992d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -538,9 +538,10 @@ GEXTEND Gram in VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri) - | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is + | IDENT "Existing"; IDENT "Instance"; is = global -> + VernacDeclareInstance (not (use_section_locality ()), is) - | IDENT "Existing"; IDENT "Class"; is = identref -> VernacDeclareClass is + | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 3ef45072cc..873558dff9 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -736,11 +736,12 @@ let rec pr_vernac = function pr_and_type_binders_arg l ++ spc () ++ str "]") - | VernacDeclareInstance id -> - hov 1 (str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_lident id) + | VernacDeclareInstance (glob, id) -> + hov 1 (pr_non_locality (not glob) ++ + str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_reference id) | VernacDeclareClass id -> - hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id) + hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id) (* Modules and Module Types *) | VernacDefineModule (export,m,bl,tys,bd) -> |