Change Hint Resolve, Immediate to take a global reference as argument

instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


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

4 files changed, 31 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 47b89e9af..b20caf450 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -560,7 +560,8 @@ let make_extern pri pat tacast =
      name = PathAny;
      code = Extern tacast })
 
-let make_trivial env sigma ?(name=PathAny) c =
+let make_trivial env sigma ?(name=PathAny) r =
+  let c = constr_of_global 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
@@ -716,8 +717,9 @@ let add_resolves env sigma clist local dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (local,dbname, AddHints
-     	      (List.flatten (List.map (fun (x, hnf, path, y) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
+     	      (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)))))
     dbnames
 
 let add_unfolds l local dbnames =
@@ -772,8 +774,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 * constr) list
-  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
@@ -813,24 +815,19 @@ let prepare_hint env (sigma,c) =
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
 
-let path_of_constr_expr c =
-  match c with
-  | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny)
-  | _ -> PathAny
-      
 let interp_hints h =
-  let f c =
-    let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
-    let c = prepare_hint (Global.env()) (evd,c) in
-    Evarutil.check_evars (Global.env()) Evd.empty evd c;
-    c in
   let fr r =
     let gr = global_with_alias r in
     let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
     r' in
-  let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in
-  let fi c = path_of_constr_expr c, f c in
+  let fres (o, b, c) =
+    let gr = global_with_alias c in
+      (o, b, PathHints [gr], gr) in
+  let fi c =
+    let gr = global_with_alias c in
+      PathHints [gr], gr
+  in
   let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
@@ -843,7 +840,8 @@ let interp_hints h =
         let ind = global_inductive_with_alias qid in
 	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
         List.tabulate (fun i -> let c = (ind,i+1) in
-			 None, true, PathHints [ConstructRef c], mkConstruct c)
+				let gr = ConstructRef c in
+			 None, true, PathHints [gr], 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 094030bea..de1d2ff6b 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 * constr) list
-  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference) 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 1fc013496..f2f5417ef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -250,7 +250,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	  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 c) 
+		  (true,false,Flags.is_verbose()) pri (constr_of_global c))
 	       hints)
 	else []
       in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c2d5de265..1c9833571 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -273,9 +273,10 @@ END
 open Term
 open Coqlib
 
-let project_hint pri l2r c =
+let project_hint pri l2r r =
+  let gr = Smartlocate.global_with_alias r in
   let env = Global.env() in
-  let c = Constrintern.interp_constr Evd.empty env c in
+  let c = Globnames.constr_of_global gr in
   let t = Retyping.get_type_of env Evd.empty c in
   let t =
     Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
@@ -288,24 +289,28 @@ let project_hint pri l2r c =
   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
-  (pri,true,Auto.PathAny,c)
+  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)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
     (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
 
 VERNAC COMMAND EXTEND HintResolveIffLR
-  [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+  [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff true lc n bl ]
-| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
   [ add_hints_iff true lc n ["core"] ]
 END
 VERNAC COMMAND EXTEND HintResolveIffRL
-  [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+  [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff false lc n bl ]
-| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
   [ add_hints_iff false lc n ["core"] ]
 END