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

8 files changed, 28 insertions, 28 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) ->
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index ce6abc93ec..50a735e58c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -825,6 +825,9 @@ let merge_evars (goal,cstr) = Evd.merge goal cstr
 let solve_constraints env evars =
   Typeclasses.resolve_typeclasses env ~split:false ~fail:true (merge_evars evars)
 
+let nf_zeta =
+  Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+
 let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
   let concl, is_hyp =
     match clause with
@@ -848,6 +851,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	    let cstrevars = !evars in
 	    let evars = solve_constraints env cstrevars in
 	    let p = Evarutil.nf_isevar evars p in
+	    let p = nf_zeta env evars p in
 	    let newt = Evarutil.nf_isevar evars newt in
 	    let abs = Option.map (fun (x, y) ->
 	      Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 90d0d0e007..515d9519f8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -262,7 +262,7 @@ module Latex = struct
 	    (printf "\\coqref{"; label_ident id; printf "}{\\coqdoc%s{" (type_name typ);
 	     raw_ident s; printf "}}")
       | External m when !externals ->
-	  printf "\\coqexternalref{"; label_ident m; printf "}{";
+	  printf "\\coqexternalref{"; raw_ident m; printf "}{";
 	  label_ident fid; printf "}{\\coqdoc%s{" (type_name typ); raw_ident s; printf "}}"
       | External _ | Unknown ->
 	  (* printf "\\coqref{"; label_ident id; printf "}{" *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 33b7dd0979..5eabc852d8 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 5953c14f94..c8439a1668 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 69a76bcc8c..a90136d43e 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 d0ee9d39cf..5be5c940b5 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 *