diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Classes/SetoidTactics.v | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 145d451f..190397ae 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := - setoidreplace (default_relation x y) ltac:t. + setoidreplace (default_relation x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (default_relation x y) ltac:t o. + setoidreplaceat (default_relation x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (default_relation x y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (default_relation x y) id ltac:t o. + setoidreplaceinat (default_relation x y) id ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := @@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "by" tactic3(t) := - setoidreplace (rel x y) ltac:t. + setoidreplace (rel x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (rel x y) ltac:t o. + setoidreplaceat (rel x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) @@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (rel x y) id ltac:t. + setoidreplacein (rel x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (rel x y) id ltac:t o. + setoidreplaceinat (rel x y) id ltac:(t) o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back to the user to discharge the |