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

4 files changed, 16 insertions, 22 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 33b7dd097..5eabc852d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -47,25 +47,21 @@ let _ =
 	      [pri, false, constr_of_global inst])) ());
   Typeclasses.register_set_typeclass_transparency set_typeclass_transparency
     
-let declare_class glob idl =
-  match global (Ident idl) with
+let declare_class g =
+  match global g with
   | ConstRef x -> Typeclasses.add_constant_class x
   | IndRef x -> Typeclasses.add_inductive_class x
-  | _ -> user_err_loc (fst idl, "declare_class", 
+  | _ -> user_err_loc (loc_of_reference g, "declare_class", 
 		      Pp.str"Unsupported class type, only constants and inductives are allowed")
     
-let declare_instance_cst glob c =
+let declare_instance glob g =
+  let c = global g in
   let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
       | Some tc -> add_instance (new_instance tc None glob c)
-      | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
-
-let declare_instance glob idl =
-  let con = 
-    try global (Ident idl)
-    with _ -> error "Instance definition not found."
-  in declare_instance_cst glob con
+      | None -> user_err_loc (loc_of_reference g, "declare_instance",
+			     Pp.str "Constant does not build instances of a declared type class.")
 
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 5953c14f9..c8439a166 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -21,6 +21,7 @@ open Topconstr
 open Util
 open Typeclasses
 open Implicit_quantifiers
+open Libnames
 (*i*)
 
 (* Errors *)
@@ -31,11 +32,11 @@ val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
 (* Post-hoc class declaration. *)
 
-val declare_class : bool -> identifier located -> unit
+val declare_class : reference -> unit
 
 (* Instance declaration *)
 
-val declare_instance : bool -> identifier located -> unit
+val declare_instance : bool -> reference -> unit
 
 val declare_instance_constant :
   typeclass ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 69a76bcc8..a90136d43 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -619,13 +619,11 @@ let vernac_context l =
   List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
   Classes.context l
 
-let vernac_declare_instance id =
-  Dumpglob.dump_definition id false "inst";
-  Classes.declare_instance false id
+let vernac_declare_instance glob id =
+  Classes.declare_instance glob id
 
 let vernac_declare_class id =
-  Dumpglob.dump_definition id false "class";
-  Classes.declare_class false id
+  Classes.declare_class id
 
 (***********)
 (* Solving *)
@@ -1344,7 +1342,7 @@ let interp c = match c with
   (* Type classes *)
   | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
   | VernacContext sup -> vernac_context sup
-  | VernacDeclareInstance id -> vernac_declare_instance id
+  | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d0ee9d39c..5be5c940b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -257,10 +257,9 @@ type vernac_expr =
   | VernacContext of local_binder list
 
   | VernacDeclareInstance of
-      lident (* instance name *)
+      bool (* global *) * reference (* instance name *)
 
-  | VernacDeclareClass of
-      lident (* inductive or definition name *)
+  | VernacDeclareClass of reference (* inductive or definition name *)
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *