eliminate race condition for opam compilation

MetaCoq · Nov 1, 2023 · 7d0a7a6 · 7d0a7a6
1 parent 045ec00
commit 7d0a7a6
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
@@ -1,6 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
 From Coq Require Import Utf8 Program.
-From MetaCoq Require Import config utils BasicAst.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import config BasicAst.
 From MetaCoq.PCUIC Require PCUICWcbvEval.
 From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst EReflect EGlobalEnv
   EWellformed EWcbvEval.
@@ -671,7 +672,7 @@ Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
 Local Hint Constructors represents : core.
 Local Hint Constructors represents_value : core.
 
-From MetaCoq Require Import bytestring MCString.
+From MetaCoq.Utils Require Import bytestring MCString.
 Require Import BinaryString.
 Import String.