diff options
| author | ppedrot | 2013-05-12 15:33:40 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-12 15:33:40 +0000 |
| commit | de26e97cf37cafd37b83377d2df062a6e82676e7 (patch) | |
| tree | 1f093c94b7cb8ab59f301b9c5ee7ca712aa9fa0f /tactics/rewrite.ml4 | |
| parent | 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 (diff) | |
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
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 5722c11eae..0e6654545d 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 ] |