From 42ea537affb88f8e63499d909eb526e024fc0aec Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 27 Dec 2009 22:08:57 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 5 +++--
 parsing/ppvernac.ml  | 7 ++++---
 2 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'parsing')

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) ->
-- 
cgit v1.2.3