From 1c553b9f958e851c4182d17febc55bfb90b9302b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Aug 2016 15:14:57 +0200
Subject: [PATCH] Fix levels of arguments in proof mode terms.
---
proofmode/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 404eb149b..eca089bfb 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -128,9 +128,9 @@ Record iTrm {X As} :=
Arguments ITrm {_ _} _ _ _.
Notation "( H $! x1 .. xn )" :=
- (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 0).
+ (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
Notation "( H $! x1 .. xn 'with' pat )" :=
- (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
+ (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
--
GitLab