diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-26 16:57:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-26 16:57:26 +0000 |
| commit | 7e5ae3dc23fb4823f8ff8851a01023733fc056f8 (patch) | |
| tree | 93575dea82ce032348f82061230854301dc8aad5 /tactics/equality.mli | |
| parent | 781f9487907a301282b17452ad8cf596077cd896 (diff) | |
Even better test for choosing rewrite or setoid_rewrite.
Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 3c7f9c6b0..0f93784af 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -45,6 +45,7 @@ val rewriteRL : constr -> tactic val register_general_setoid_rewrite_clause : (identifier option -> bool -> occurrences -> constr -> new_goals:constr list -> tactic) -> unit +val register_is_applied_setoid_relation : (constr -> bool) -> unit val general_rewrite_bindings_in : bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic |