Use the Hook module here and there.

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

10 files changed, 60 insertions, 82 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5aab5f252..f12bddfb7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -643,10 +643,7 @@ let cache_autohint (_,(local,name,hints)) =
   | RemoveHints grs -> remove_hint name grs
   | AddCut path -> add_cut name path
 
-let forward_subst_tactic =
-  ref (fun _ -> failwith "subst_tactic is not installed for auto")
-
-let set_extern_subst_tactic f = forward_subst_tactic := f
+let (forward_subst_tactic, extern_subst_tactic) = Hook.make ()
 
 let subst_autohint (subst,(local,name,hintlist as obj)) =
   let subst_key gr =
@@ -679,7 +676,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code else Unfold_nth ref'
       | Extern tac ->
-	  let tac' = !forward_subst_tactic subst tac in
+	  let tac' = Hook.get forward_subst_tactic subst tac in
 	  if tac==tac' then data.code else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
@@ -793,10 +790,7 @@ let add_trivials env sigma l local dbnames =
 		    AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l))))
     dbnames
 
-let forward_intern_tac =
-  ref (fun _ -> failwith "intern_tac is not installed for auto")
-
-let set_extern_intern_tac f = forward_intern_tac := f
+let (forward_intern_tac, extern_intern_tac) = Hook.make ()
 
 type hints_entry =
   | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
@@ -880,7 +874,8 @@ let interp_hints =
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
-      let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
+      let l = match pat with None -> [] | Some (l, _) -> l in
+      let tacexp = Hook.get forward_intern_tac l tacexp in
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
@@ -1104,10 +1099,7 @@ si après Intros la conclusion matche le pattern.
 
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
-let forward_interp_tactic =
-  ref (fun _ -> failwith "interp_tactic is not installed for auto")
-
-let set_extern_interp f = forward_interp_tactic := f
+let (forward_interp_tactic, extern_interp) = Hook.make ()
 
 let conclPattern concl pat tac gl =
   let constr_bindings =
@@ -1116,7 +1108,7 @@ let conclPattern concl pat tac gl =
     | Some pat ->
 	try matches pat concl
 	with PatternMatchingFailure -> error "conclPattern" in
-    !forward_interp_tactic constr_bindings tac gl
+    Hook.get forward_interp_tactic constr_bindings tac gl
 
 (***********************************************************)
 (** A debugging / verbosity framework for trivial and auto *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 99f4768c2..2a163120a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -173,16 +173,14 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
-val set_extern_interp :
-  (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit
+val extern_interp :
+  (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) Hook.t
 
-val set_extern_intern_tac :
-  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr)
-  -> unit
+val extern_intern_tac :
+  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
-val set_extern_subst_tactic :
-  (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
-  -> unit
+val extern_subst_tactic :
+  (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2dc42e35f..b0bcf57d7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -228,11 +228,8 @@ let general_elim_clause with_evars frzevars tac cls sigma c t l l2r elim gl =
   If occurrences are set, use general rewrite.
 *)
 
-let general_rewrite_clause = ref (fun _ -> assert false)
-let register_general_rewrite_clause = (:=) general_rewrite_clause
-
-let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
-let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
+let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
+let (forward_is_applied_rewrite_relation, is_applied_rewrite_relation) = Hook.make ()
 
 (* Do we have a JMeq instance on twice the same domains ? *)
 
@@ -331,7 +328,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars gl =
   if occs != AllOccurrences then (
-    rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
+    rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
   else
     let env = pf_env gl in
     let sigma = project gl in
@@ -344,7 +341,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	    l with_evars frzevars dep_proof_ok gl hdcncl
       | None ->
 	  try
-	    rewrite_side_tac (!general_rewrite_clause cls
+	    rewrite_side_tac (Hook.get forward_general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
 	  with e when Errors.noncritical e ->
             (* Try to see if there's an equality hidden *)
@@ -1562,7 +1559,8 @@ let replace_multi_term dir_opt c  =
   in
   rewrite_multi_assumption_cond cond_eq_fun
 
-let _ = Tactics.register_general_multi_rewrite
-  (fun b evars t cls -> general_multi_rewrite b evars t cls)
+let _ =
+  let gmr l2r with_evars tac c = general_multi_rewrite l2r with_evars tac c in
+  Hook.set Tactics.general_multi_rewrite gmr
 
-let _ = Tactics.register_subst_one (fun b -> subst_one b)
+let _ = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/equality.mli b/tactics/equality.mli
index aa1bfaa0f..147218efd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -51,10 +51,10 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr  -> tactic
 
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
-val register_general_rewrite_clause :
+val general_rewrite_clause :
   (Id.t option -> orientation ->
-    occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit
-val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
+    occurrences -> constr with_bindings -> new_goals:constr list -> tactic) Hook.t
+val is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) Hook.t
 
 val general_rewrite_ebindings_clause : Id.t option ->
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 5722c11ea..0e6654545 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -123,7 +123,7 @@ let is_applied_rewrite_relation env sigma rels t =
   | _ -> None
 
 let _ =
-  Equality.register_is_applied_rewrite_relation is_applied_rewrite_relation
+  Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation
 
 let split_head = function
     hd :: tl -> hd, tl
@@ -1970,7 +1970,7 @@ let general_s_rewrite_clause x =
     | None -> general_s_rewrite None
     | Some id -> general_s_rewrite (Some id)
 
-let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
+let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
@@ -2032,10 +2032,10 @@ let setoid_symmetry_in id gl =
 	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
       gl
 
-let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
-let _ = Tactics.register_setoid_symmetry setoid_symmetry
-let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
-let _ = Tactics.register_setoid_transitivity setoid_transitivity
+let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
+let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
+let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
+let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
 
 TACTIC EXTEND setoid_symmetry
    [ "setoid_symmetry" ] -> [ setoid_symmetry ]
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6a1a33fb0..b7108f4d3 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -983,7 +983,8 @@ let add_tacdef local isrec tacl =
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
-let _ = Auto.set_extern_intern_tac
-  (fun l ->
-    Flags.with_option strict_check
-    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])}))
+let _ =
+  let f l = Flags.with_option strict_check
+    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])})
+  in
+  Hook.set Auto.extern_intern_tac f
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index da0a3c7d9..26f7d02b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2023,7 +2023,7 @@ let tacticIn t =
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
-let _ = Auto.set_extern_interp
+let _ = Hook.set Auto.extern_interp
   (fun l ->
     let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
     interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 90739a4e9..1cf4264ea 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -347,4 +347,4 @@ and subst_genarg subst (x:glob_generic_argument) =
       | None ->
           lookup_genarg_subst s subst x
 
-let _ = Auto.set_extern_subst_tactic subst_tactic
+let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0599c52d1..ab962a4cc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1286,18 +1286,10 @@ let simplest_split = split NoBindings
 (*****************************)
 
 (* Rewriting function for rewriting one hypothesis at the time *)
-let forward_general_multi_rewrite =
-  ref (fun _ -> failwith "general_multi_rewrite undefined")
+let (forward_general_multi_rewrite, general_multi_rewrite) = Hook.make ()
 
 (* Rewriting function for substitution (x=t) everywhere at the same time *)
-let forward_subst_one =
-  ref (fun _ -> failwith "subst_one undefined")
-
-let register_general_multi_rewrite f =
-  forward_general_multi_rewrite := f
-
-let register_subst_one f =
-  forward_subst_one := f
+let (forward_subst_one, subst_one) = Hook.make ()
 
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
@@ -1331,9 +1323,9 @@ let intro_or_and_pattern loc b ll l' tac id gl =
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
-    !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
+    Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
   let subst_on l2r x rhs =
-    !forward_subst_one true x (id,rhs,l2r) in
+    Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
   let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
@@ -1444,7 +1436,7 @@ let prepare_intros s ipat gl = match ipat with
   | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
   | IntroRewrite l2r ->
       let id = make_id s gl in
-      id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | IntroOrAndPattern ll -> make_id s gl,
       onLastHypId
 	(intro_or_and_pattern loc true ll []
@@ -1479,7 +1471,7 @@ let assert_tac na = assert_as true (ipat_of_name na)
 
 let as_tac id ipat = match ipat with
   | Some (loc,IntroRewrite l2r) ->
-      !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll []
         (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards))
@@ -3371,8 +3363,7 @@ let dImp cls =
 
 (* Reflexivity tactics *)
 
-let setoid_reflexivity = ref (fun _ -> assert false)
-let register_setoid_reflexivity f = setoid_reflexivity := f
+let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let reflexivity_red allowred gl =
   (* PL: usual reflexivity don't perform any reduction when searching
@@ -3386,7 +3377,8 @@ let reflexivity_red allowred gl =
     | Some _ -> one_constructor 1 NoBindings gl
 
 let reflexivity gl =
-  try reflexivity_red false gl with NoEquationFound -> !setoid_reflexivity gl
+  try reflexivity_red false gl
+  with NoEquationFound -> Hook.get forward_setoid_reflexivity gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -3397,8 +3389,7 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
    defined and the conclusion is a=b, it solves the goal doing (Cut
    b=a;Intro H;Case H;Constructor 1) *)
 
-let setoid_symmetry = ref (fun _ -> assert false)
-let register_setoid_symmetry f = setoid_symmetry := f
+let (forward_setoid_symmetry, setoid_symmetry) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_symmetry hdcncl eq_kind =
@@ -3428,10 +3419,9 @@ let symmetry_red allowred gl =
   | None,eq,eq_kind -> prove_symmetry eq eq_kind gl
 
 let symmetry gl =
-  try symmetry_red false gl with NoEquationFound -> !setoid_symmetry gl
+  try symmetry_red false gl with NoEquationFound -> Hook.get forward_setoid_symmetry gl
 
-let setoid_symmetry_in = ref (fun _ _ -> assert false)
-let register_setoid_symmetry_in f = setoid_symmetry_in := f
+let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
@@ -3446,7 +3436,7 @@ let symmetry_in id gl =
       [ intro_replacing id;
         tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
       gl
-  with NoEquationFound -> !setoid_symmetry_in id gl
+  with NoEquationFound -> Hook.get forward_setoid_symmetry_in id gl
 
 let intros_symmetry =
   onClause
@@ -3466,8 +3456,7 @@ let intros_symmetry =
    --Eduardo (19/8/97)
 *)
 
-let setoid_transitivity = ref (fun _ _ -> assert false)
-let register_setoid_transitivity f = setoid_transitivity := f
+let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t gl =
@@ -3509,7 +3498,7 @@ let transitivity_red allowred t gl =
 
 let transitivity_gen t gl =
   try transitivity_red false t gl
-  with NoEquationFound -> !setoid_transitivity t gl
+  with NoEquationFound -> Hook.get forward_setoid_transitivity t gl
 
 let etransitivity = transitivity_gen None
 let transitivity t = transitivity_gen (Some t)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2b45ecde6..7c0fee5c7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -337,19 +337,19 @@ val simplest_split       : tactic
 
 (** {6 Logical connective tactics. } *)
 
-val register_setoid_reflexivity : tactic -> unit
+val setoid_reflexivity          : tactic Hook.t
 val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
-val register_setoid_symmetry : tactic -> unit
+val setoid_symmetry             : tactic Hook.t
 val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
-val register_setoid_symmetry_in : (Id.t -> tactic) -> unit
+val setoid_symmetry_in          : (Id.t -> tactic) Hook.t
 val symmetry_in                 : Id.t -> tactic
 val intros_symmetry             : clause -> tactic
 
-val register_setoid_transitivity : (constr option -> tactic) -> unit
+val setoid_transitivity         : (constr option -> tactic) Hook.t
 val transitivity_red            : bool -> constr option -> tactic
 val transitivity                : constr -> tactic
 val etransitivity               : tactic
@@ -385,8 +385,8 @@ val admit_as_an_axiom : tactic
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> tactic
 val specialize_eqs : Id.t -> tactic
 
-val register_general_multi_rewrite :
-  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
+val general_multi_rewrite :
+  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) Hook.t
 
-val register_subst_one :
-  (bool -> Id.t -> Id.t * constr * bool -> tactic) -> unit
+val subst_one :
+  (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t