diff options
| author | letouzey | 2006-05-02 20:59:21 +0000 |
|---|---|---|
| committer | letouzey | 2006-05-02 20:59:21 +0000 |
| commit | f07684f5d77802f8ed286fdbf234bd542b689e45 (patch) | |
| tree | eea03ce5aa629c5ce088c28ef49b86f8ebe74118 /tactics/setoid_replace.mli | |
| parent | ca2bca80347b0983e9a0b420360121ef82d72c71 (diff) | |
Changement de comportement de rewrite: face a une egalité setoid, on
arrete de reduire brutalement pour essayer de tomber sur une egalité
Coq. Au contraire, si la relation de tete est une relation declarée
dans la base des setoids, on l'utilise.
ATTENTION: ceci brise la compatibilité, dans le cas très improbable
ou quelqu'un aurait defini un setoid mais exploiterait la "feature"
de la reduction vers l'eventuelle egalité Coq sous-jacente.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8779 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 09fb39da8b..b8bed63c54 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -75,3 +75,6 @@ val add_setoid : val new_named_morphism : Names.identifier -> constr_expr -> morphism_signature option -> unit + +val relation_table_find : constr -> relation +val relation_table_mem : constr -> bool |