Fix unqualified, ambiguous imports

MetaCoq · Nov 15, 2023 · cc87a0f · cc87a0f
1 parent 9dee1c1
commit cc87a0f
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 11 deletions.
diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v
@@ -5,10 +5,9 @@ From MetaCoq.Utils Require Import bytestring utils.
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram.
 From MetaCoq.PCUIC Require Import PCUICNormal.
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnvImpl.
-From MetaCoq.Erasure Require EAstUtils ErasureCorrectness EPretty Extract.
-From MetaCoq Require Import ETransform EConstructorsAsBlocks.
+From MetaCoq.Erasure Require EAstUtils ErasureCorrectness EPretty Extract EConstructorsAsBlocks.
 From MetaCoq.Erasure Require Import EWcbvEvalNamed ErasureFunction ErasureFunctionProperties.
-From MetaCoq.ErasurePlugin Require Import Erasure.
+From MetaCoq.ErasurePlugin Require Import ETransform Erasure.
 Import PCUICProgram.
 Import PCUICTransform (template_to_pcuic_transform, pcuic_expand_lets_transform).
 

diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
@@ -1,9 +1,14 @@
 (* Distributed under the terms of the MIT license. *)
 From Coq Require Import Utf8 Program.
-From MetaCoq Require Import config utils BasicAst.
+From MetaCoq.Common Require Import config BasicAst.
+From MetaCoq.Utils Require Import utils.
 From MetaCoq.PCUIC Require PCUICWcbvEval.
 From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst EReflect EGlobalEnv
   EWellformed EWcbvEval.
+From MetaCoq.Utils Require Import bytestring MCString.
+From MetaCoq.Erasure Require Import EWcbvEvalCstrsAsBlocksFixLambdaInd.
+From Coq Require Import BinaryString.
+Import String.
 
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -671,10 +676,6 @@ 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.
-Require Import BinaryString.
-Import String.
-
 Fixpoint gen_fresh_aux (na : ident) (Γ : list string) i :=
   match i with
   | 0 => na
@@ -1559,8 +1560,6 @@ Proof.
     + eapply All2_All2_Set, All2_app. eapply H1; eauto. econstructor; eauto.
 Qed.
 
-From MetaCoq Require Import EWcbvEvalCstrsAsBlocksFixLambdaInd.
-
 Lemma lookup_in_env Σ Σ' ind i :
   All2 (fun d d' => d.1 = d'.1 × match d.2 with ConstantDecl (Build_constant_body (Some body)) =>
     ∑ body', d'.2 = ConstantDecl (Build_constant_body (Some body')) × [] ;;; [] ⊩ body' ~ body

diff --git a/test-suite/bug441.v b/test-suite/bug441.v
@@ -1,4 +1,4 @@
-From MetaCoq Require Import Template.All.
+From MetaCoq.Template Require Import All.
 Import MCMonadNotation.
 
 #[local] Existing Instance TemplateMonad_OptimizedMonad.