Skip to content

Commit e622b43

Browse files
committed
Make reordering function transparent so it can compute in Coq
1 parent e896e06 commit e622b43

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

erasure/theories/EReorderCstrs.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
From Coq Require Import List String Arith Lia.
22
Import ListNotations.
33
From Equations Require Import Equations.
4+
Set Equations Transparent.
45

56
From MetaCoq.PCUIC Require Import PCUICAstUtils.
67
From MetaCoq.Utils Require Import MCList bytestring utils monad_utils.

0 commit comments

Comments
 (0)