aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Psatz.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/Psatz.v')
-rw-r--r--plugins/micromega/Psatz.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 50e0033e5..ba1f8956e 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -69,7 +69,7 @@ Ltac xpsatz dom d :=
end in tac.
Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
-Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
Ltac psatzl dom :=
let tac := lazymatch dom with