Fix unqualified, ambiguous imports

Author: mattam82

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).
 

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

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.