Skip to content

Commit ad7ba45

Browse files
committed
don't rely on Program.Syntax re-exporting ListNotations
overlay for rocq-prover/rocq#11992
1 parent 016a240 commit ad7ba45

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

theories/Programming/Extras.v

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
Require Import Coq.Program.Syntax.
21
Require Import List.
32
Require Import String.
43

@@ -7,7 +6,7 @@ Require Import ExtLib.Core.RelDec.
76
(*Require Import Injection. *)
87

98
Open Scope string_scope.
10-
Import MonadNotation.
9+
Import MonadNotation ListNotations.
1110
Open Scope monad_scope.
1211

1312
Set Implicit Arguments.

0 commit comments

Comments
 (0)