fix benchmarks

CertiCoq · Jan 28, 2025 · 91fac85 · 91fac85
1 parent fc022f7
commit 91fac85
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/benchmarks/lib/vs.v b/benchmarks/lib/vs.v
@@ -425,9 +425,9 @@ pure atoms *)
 
 Inductive pure_atom := Eqv : expr -> expr -> pure_atom.
 
-Let var1 : var := Z2id 1.
-Let var0 : var := Z2id 0.
-Let var2 : var := Z2id 2.
+Definition var1 : var := Z2id 1.
+Definition var0 : var := Z2id 0.
+Definition var2 : var := Z2id 2.
 
 Fixpoint list_prio {A} (weight: var) (l: list A) (p: var) : var :=
   match l with