From dfe6aadd08ba5cb9f689f3d125cba2fa78f20e79 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Fri, 23 Jul 2004 14:07:09 +0000 Subject: Since setoid_{replace,rewrite} now uses replace there is a circularity involving the two modules Equality and Setoid_replace. Resolved by making equality register the replace function to the Setoid_replace module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5971 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tactics/equality.ml b/tactics/equality.ml index e836625d8..fc2ce75f2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1211,3 +1211,5 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t) let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t) let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t) + +let _ = Setoid_replace.register_replace replace -- cgit v1.2.3