From 49e63a2713f04d35a56cda920a5646678f752a58 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 15 Oct 2004 16:26:05 +0000
Subject: Wrong comment committed. The tactic behaves correctly only when the
 relation/morphisms are quantified using LetIns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 4e17fef9ed..54c961ed30 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1000,8 +1000,6 @@ let int_add_relation id a aeq refl sym trans =
            const_entry_opaque = false},
           IsDefinition)
       in
-       (*CSCXX: bug here; if there is a LetIn this code is completely brain
-         damaged*)
        let a_quantifiers_rev =
         List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
        add_morphism None mor_name
@@ -1061,8 +1059,9 @@ let add_setoid id a aeq th =
         const_entry_type = None;
         const_entry_opaque = false},
        IsDefinition) in
-   (*CSCXX: bug here; if there is a LetIn this code is completely brain damaged*)
-   let a_quantifiers_rev = List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
+   let a_quantifiers_rev =
+    List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev
+   in
     add_morphism None mor_name
      (aeq,a_quantifiers_rev,[aeq_rel_class_and_var ; aeq_rel_class_and_var],
        Lazy.force coq_iff_relation)
-- 
cgit v1.2.3