From c52756a8fda857b0b7051a73d3afbb90aa5be5e9 Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Sun, 3 May 2020 01:50:40 +0200
Subject: Ensure eintros allows creating evars

Thread the `ev` (an `evar_flag`) appropriately through `intros0`.
Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
---
 user-contrib/Ltac2/Notations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
-- 
cgit v1.2.3