Make reordering function transparent so it can compute in Coq

MetaCoq · Feb 21, 2024 · e622b43 · e622b43
1 parent e896e06
commit e622b43
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v
@@ -1,6 +1,7 @@
 From Coq Require Import List String Arith Lia.
 Import ListNotations.
 From Equations Require Import Equations.
+Set Equations Transparent.
 
 From MetaCoq.PCUIC Require Import PCUICAstUtils.
 From MetaCoq.Utils Require Import MCList bytestring utils monad_utils.