aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/CMorphisms.v2
-rw-r--r--theories/Classes/Morphisms.v2
-rw-r--r--theories/Classes/SetoidTactics.v16
3 files changed, 10 insertions, 10 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 10f18fe70..1cfca4169 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -452,7 +452,7 @@ Ltac partial_application_tactic :=
let rec do_partial_apps H m cont :=
match m with
| ?m' ?x => class_apply @Reflexive_partial_app_morphism ;
- [(do_partial_apps H m' ltac:idtac)|clear H]
+ [(do_partial_apps H m' ltac:(idtac))|clear H]
| _ => cont
end
in
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8d942d908..81b31d783 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -465,7 +465,7 @@ Ltac partial_application_tactic :=
let rec do_partial_apps H m cont :=
match m with
| ?m' ?x => class_apply @Reflexive_partial_app_morphism ;
- [(do_partial_apps H m' ltac:idtac)|clear H]
+ [(do_partial_apps H m' ltac:(idtac))|clear H]
| _ => cont
end
in
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 145d451f0..190397ae4 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