diff options
| -rw-r--r-- | user-contrib/Ltac2/Notations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index 373654e6db..390b39bab1 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -146,7 +146,7 @@ match ev with end. Ltac2 intros0 ev p := - Control.enter (fun () => Std.intros false p). + Control.enter (fun () => Std.intros ev p). Ltac2 Notation "intros" p(intropatterns) := intros0 false p. Ltac2 Notation intros := intros. |