diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:13:08 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:13:08 +0000 |
| commit | 145ad94fc96a4989c24061de7a90b7520d530932 (patch) | |
| tree | f3a8882c9da47fddbbd61c22ef01f42fefae5f67 /theories/Classes/SetoidTactics.v | |
| parent | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (diff) | |
Document the new setoid rewrite tactic, and fix a few things while
testing:
- better? pretty printing
- correct handling of load/open/cache
- do less reduction in build_signature, commited in previous patch. May
break some scripts (but Parametric will break more and before :).
- remove ===def notation as suggested by A. Spiwack.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 9d3648fef..03195e083 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -36,16 +36,16 @@ Ltac setoidreplacein H H' t := cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ]. Tactic Notation "setoid_replace" constr(x) "with" constr(y) := - setoidreplace (x ===def y) idtac. + setoidreplace (default_relation x y) idtac. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) := - setoidreplacein (x ===def y) id idtac. + setoidreplacein (default_relation x y) id idtac. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) := - setoidreplace (x ===def y) ltac:t. + setoidreplace (default_relation x y) ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) := - setoidreplacein (x ===def y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := setoidreplace (rel x y) idtac. |