diff options
| author | Paolo G. Giarrusso | 2020-05-03 01:50:40 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-05-03 01:50:40 +0200 |
| commit | c52756a8fda857b0b7051a73d3afbb90aa5be5e9 (patch) | |
| tree | c75c8cf07dfebba6d855a33970e57339d410f757 /user-contrib/Ltac2/Notations.v | |
| parent | f129326d545ae27d362132b279167d119894a992 (diff) | |
Ensure eintros allows creating evars
Thread the `ev` (an `evar_flag`) appropriately through `intros0`.
Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
Diffstat (limited to 'user-contrib/Ltac2/Notations.v')
| -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. |