diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-15 16:26:05 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-15 16:26:05 +0000 |
| commit | 49e63a2713f04d35a56cda920a5646678f752a58 (patch) | |
| tree | d56509589de04d3e5d1fe37ab82872592db9b498 | |
| parent | 9cd887e95a320d22c8158888a996fa6e50fd1189 (diff) | |
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
| -rw-r--r-- | tactics/setoid_replace.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4e17fef9e..54c961ed3 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) |