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

4 files changed, 20 insertions, 26 deletions

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