Commit 1c553b9f authored by Robbert Krebbers's avatar Robbert Krebbers

Fix levels of arguments in proof mode terms.

parent 90cbf2a0
Pipeline #2555 passed with stage
in 3 minutes and 57 seconds
......@@ -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) :=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment