diff options
| author | Kenji Maillard | 2020-05-10 11:52:43 +0200 |
|---|---|---|
| committer | Kenji Maillard | 2020-05-10 11:52:43 +0200 |
| commit | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (patch) | |
| tree | 6b5147717989fdbe99e2d4e4690f7de736c1b15f | |
| parent | d567eeeac238175e4d3d032f72a1409145abf89d (diff) | |
| parent | c52756a8fda857b0b7051a73d3afbb90aa5be5e9 (diff) | |
Merge PR #12235: Ensure eintros allows creating evars
Reviewed-by: kyoDralliam
| -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. |