Skip to content

Commit 016a240

Browse files
mattam82liyishuai
authored andcommitted
Fix for Coq 8.11
1 parent 20dedfe commit 016a240

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

theories/Data/SumN.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ From Coq Require Import PArith.
22
Require Import ExtLib.Data.Map.FMapPositive.
33
Require Import ExtLib.Data.Eq.
44
Require Import ExtLib.Tactics.Injection.
5+
From Coq Require Import PArith.
56

67
Fixpoint pmap_lookup' (ts : pmap Type) (p : positive) : option Type :=
78
match p with

0 commit comments

Comments
 (0)