Finish patch for Hint Resolve, stopping to generate new constant names for

hints. 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 59 insertions, 56 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 81cb241c9..b5312e574 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -128,6 +128,14 @@ module ExtRefOrdered = struct
       | _, _ -> Pervasives.compare x y
 end
 
+type global_reference_or_constr = 
+  | IsGlobal of global_reference
+  | IsConstr of constr
+
+let constr_of_global_or_constr = function
+  | IsConstr c -> c
+  | IsGlobal gr -> constr_of_global gr
+
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
 let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
diff --git a/library/globnames.mli b/library/globnames.mli
index 02ac51fb1..af1f10ee4 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -72,6 +72,12 @@ module ExtRefOrdered : sig
   val compare : t -> t -> int
 end
 
+type global_reference_or_constr = 
+  | IsGlobal of global_reference
+  | IsConstr of constr
+
+val constr_of_global_or_constr : global_reference_or_constr -> constr
+
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
 val encode_mind : dir_path -> identifier -> mutual_inductive
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7d9d0bbd8..b5c710da2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -20,7 +20,7 @@ open Libobject
 (*i*)
 
 
-let add_instance_hint_ref = ref (fun id local pri -> assert false)
+let add_instance_hint_ref = ref (fun id path local pri -> assert false)
 let register_add_instance_hint =
   (:=) add_instance_hint_ref
 let add_instance_hint id = !add_instance_hint_ref id
@@ -39,11 +39,6 @@ let classes_transparent_state_ref = ref (fun () -> assert false)
 let register_classes_transparent_state = (:=) classes_transparent_state_ref
 let classes_transparent_state () = !classes_transparent_state_ref ()
 
-
-let declare_definition_ref = ref (fun ?internal ?opaque ?kind id ?types constr -> assert false)
-let register_declare_definition =
-  (:=) declare_definition_ref
-
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_one_typeclass env evm t =
@@ -247,18 +242,20 @@ let check_instance env sigma c =
   with _ -> false
 
 let build_subclasses ~check env sigma glob pri =
-  let id = Nametab.basename_of_global glob in
-  let next_id = 
+  let _id = Nametab.basename_of_global glob in
+  let _next_id = 
     let i = ref (-1) in 
       (fun () -> incr i;
-        Nameops.add_suffix id ("_subinstance_" ^ string_of_int !i))
+        Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
-  let rec aux pri c =
+  let rec aux pri c path =
     let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
       match class_of_constr ty with
       | None -> []
       | Some (rels, (tc, args)) ->
-	let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in
+	let instapp = 
+	  Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) 
+	in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
 	  (fun (n, b, proj) ->
@@ -276,16 +273,14 @@ let build_subclasses ~check env sigma glob pri =
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		 let c = !declare_definition_ref ~internal:true
-		   ~kind:Decl_kinds.Instance (next_id ()) body 
-		 in
-		   Some (ConstRef proj, pri, ConstRef c)) tc.cl_projs 
+		   Some (ConstRef proj, pri, body)) tc.cl_projs 
 	in
 	let declare_proj hints (cref, pri, body) =
-	  let rest = aux pri (constr_of_global body) in
-	    hints @ (pri, body) :: rest
+	  let path' = cref :: path in
+	  let rest = aux pri body path' in
+	    hints @ (path', pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
-  in aux pri (constr_of_global glob)
+  in aux pri (constr_of_global glob) [glob]
 
 (*
  * instances persistent object
@@ -331,8 +326,9 @@ let discharge_instance (_, (action, inst)) =
 let is_local i = Int.equal i.is_global (-1)
 
 let add_instance check inst =
-  add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
-  List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri) 
+  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) inst.is_pri;
+  List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
+    (is_local inst) pri) 
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) Evd.empty inst.is_impl inst.is_pri)
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 729cbb2ad..72b3bbd27 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,13 +103,12 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val register_classes_transparent_state : (unit -> transparent_state) -> unit
 val classes_transparent_state : unit -> transparent_state
 
-val register_declare_definition : (?internal:bool -> ?opaque:bool -> ?kind:definition_object_kind -> identifier -> ?types:constr -> constr -> constant) -> unit
-
-
 val register_add_instance_hint : 
-  (global_reference -> bool (* local? *) -> int option -> unit) -> unit
+  (global_reference_or_constr -> global_reference list -> 
+   bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : global_reference -> bool -> int option -> unit
+val add_instance_hint : global_reference_or_constr -> global_reference list -> 
+  bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
@@ -123,4 +122,4 @@ val declare_instance : int option -> bool -> global_reference -> unit
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (int option * global_reference) list
+  (global_reference list * int option * constr) list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b626e662d..a462460a5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -574,10 +574,10 @@ let make_extern pri pat tacast =
    { pri = pri;
      pat = pat;
      name = PathAny;
-     code = Extern tacast })
+     code = Extern tacast })  
 
 let make_trivial env sigma ?(name=PathAny) r =
-  let c = constr_of_global r in
+  let c = constr_of_global_or_constr r in
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
@@ -726,6 +726,8 @@ let remove_hints local dbnames grs =
 	 Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
       dbnames
 
+open Misctypes
+
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
@@ -736,8 +738,12 @@ let add_resolves env sigma clist local dbnames =
 	 (inAutoHint
 	    (local,dbname, AddHints
      	      (List.flatten (List.map (fun (x, hnf, path, gr) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path 
-		  (constr_of_global gr)) clist)))))
+	        let c = 
+		  match gr with
+		  | IsConstr c -> c
+		  | IsGlobal gr -> constr_of_global gr
+		in
+		  make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path c) clist)))))
     dbnames
 
 let add_unfolds l local dbnames =
@@ -792,8 +798,8 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
-  | HintsImmediateEntry of (hints_path_atom * global_reference) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference_or_constr) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
@@ -834,7 +840,6 @@ let prepare_hint env (sigma,c) =
   iter c
 
 let interp_hints =
-  let hint_counter = ref 1 in
   fun h ->
   let f c =
     let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
@@ -850,15 +855,8 @@ let interp_hints =
     match c with
     | HintsReference c ->
       let gr = global_with_alias c in
-	(PathHints [gr], gr)
-    | HintsConstr c ->
-      let term = f c in
-      let id = id_of_string ("auto_hint_" ^ string_of_int !hint_counter) in
-	incr hint_counter;
-      let kn = Declare.declare_definition ~internal:Declare.KernelSilent
-	~opaque:false id term in
-      let gr = ConstRef kn in
-	(PathHints [gr], gr)
+	(PathHints [gr], IsGlobal gr)
+    | HintsConstr c -> (PathAny, IsConstr (f c))
   in
   let fres (o, b, c) =
     let path, gr = fi c in
@@ -877,7 +875,7 @@ let interp_hints =
 	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
         List.tabulate (fun i -> let c = (ind,i+1) in
 				let gr = ConstructRef c in
-			 None, true, PathHints [gr], gr)
+			 None, true, PathHints [gr], IsGlobal gr)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index de1d2ff6b..b7f5a312a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -96,8 +96,8 @@ type hint_db_name = string
 type hint_db = Hint_db.t
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
-  | HintsImmediateEntry of (hints_path_atom * global_reference) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference_or_constr) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bc2e8ac2b..a18992f70 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -249,8 +249,8 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	if is_class then
 	  let hints = build_subclasses ~check:false env sigma (VarRef id) None in
 	    (List.map_append
-	       (fun (pri, c) -> make_resolves env sigma 
-		  (true,false,Flags.is_verbose()) pri (constr_of_global c))
+	       (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
+		  (true,false,Flags.is_verbose()) pri c)
 	       hints)
 	else []
       in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4e22044d5..ade53e768 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -289,11 +289,7 @@ let project_hint pri l2r r =
   let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
-  let id =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let c = Declare.declare_definition ~internal:Declare.KernelSilent id c in
-    (pri,true,Auto.PathAny, Globnames.ConstRef c)
+    (pri,true,Auto.PathAny, Globnames.IsConstr c)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 40556c4aa..df5d42bbc 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -761,7 +761,7 @@ intros x; case x; simpl ww_is_even.
   auto.
  split.
  unfold zn2z_to_Z; rewrite <- Hw1.
- unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1.
+ unfold ww_to_Z, zn2z_to_Z in H1. rewrite H1.
  rewrite <- Hw0.
  match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U =>
   transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 43caf3fa3..618ec2bc0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -24,6 +24,7 @@ open Constrexpr
 
 open Decl_kinds
 open Entries
+open Misctypes
 
 let typeclasses_db = "typeclass_instances"
 
@@ -33,12 +34,11 @@ let set_typeclass_transparency c local b =
     
 let _ =
   Typeclasses.register_add_instance_hint
-    (fun inst local pri ->
-     let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in
+    (fun inst path local pri ->
       Flags.silently (fun () ->
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
-	     [pri, false, path, inst])) ());
+	     [pri, false, Auto.PathHints path, inst])) ());
   Typeclasses.register_set_typeclass_transparency set_typeclass_transparency;
   Typeclasses.register_classes_transparent_state 
     (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))