- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence

  as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
  uglily to be factorized by hand.
- Typography in RefMan-tac.tex.



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

1 files changed, 1 insertions, 9 deletions

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index b37212d9d..3d34a2d68 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -225,16 +225,10 @@ let (inDD,_) =
 		    classify_function = classify_dd;
                     export_function = export_dd }
 
-let forward_intern_tac = 
-  ref (fun _ -> failwith "intern_tac is not installed for DHyp")
-
-let set_extern_intern_tac f = forward_intern_tac := f
-
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
     
-let add_destructor_hint local na loc pat pri code =
-  let code = !forward_intern_tac code in
+let add_destructor_hint local na loc (_,pat) pri code =
   let code =
     begin match loc, code with
       | HypLocation _, TacFun ([id],body) -> (id,body)
@@ -243,8 +237,6 @@ let add_destructor_hint local na loc pat pri code =
 	  errorlabstrm "add_destructor_hint"
           (str "The tactic should be a function of the hypothesis name.") end
   in
-  let (_,pat) = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat
-  in
   let pat = match loc with
     | HypLocation b ->
 	HypLocation