Fix require in modules

embedding/extraction/PreludeExt.v

@@ -117,8 +117,6 @@ Definition is_contract (addr: address_coq) :=
   | UserAddr_coq _ => false
   end.
 
-Print Instances countable.Countable.
-
 Definition encode_addr (addr: address_coq) : nat + nat :=
   match addr with
   | ContractAddr_coq x => inl x

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -658,7 +658,7 @@ Proof.
 Qed.
 
 
-Hint Resolve forallb_type_to_term_closed.
+Hint Resolve forallb_type_to_term_closed : core.
 
 Lemma expr_closed_term_closed e n Σ:
   genv_ok Σ ->
@@ -1145,7 +1145,7 @@ Proof.
 Qed.
 
 Remove Hints iclosed_n_geq: hints.
-Remove Hints Bool.absurd_eq_true.
+Remove Hints Bool.absurd_eq_true : core.
 
 Open Scope nat.
 
@@ -1405,7 +1405,7 @@ Proof.
   apply All_snd_combine.
 Qed.
 
-Hint Constructors All.
+Hint Constructors All : core.
 
 Lemma eval_ge_val_ok n ρ Σ e v :
   AllEnv (ge_val_ok Σ) ρ ->

execution/tests/CongressTests/Congress_BuggyTests.v

@@ -28,7 +28,7 @@ Close Scope address_scope.
 
 (* -------------------------- Tests of the Buggy Congress Implementation -------------------------- *)
 
-Let creator := BoundedN.of_Z_const AddrSize 10.
+Definition creator := BoundedN.of_Z_const AddrSize 10.
 
 Definition rules := {|
   min_vote_count_permille := 200;

execution/tests/EIP20Tests/EIP20TokenTests.v

@@ -26,7 +26,7 @@ Definition init_supply := (100%N).
 Definition token_setup := EIP20Token.build_setup creator init_supply.
 Definition deploy_eip20token := create_deployment 0 EIP20Token.contract token_setup.
 
-Let contract_base_addr := BoundedN.of_Z_const AddrSize 128%Z.
+Definition contract_base_addr := BoundedN.of_Z_const AddrSize 128%Z.
 
 (* In the initial chain we transfer some assets to a few accounts, just to make the addresses
    present in the chain state. The amount transferred is irrelevant. *)

execution/tests/FA2Tests/FA2TokenTests.v

@@ -12,6 +12,7 @@ From ExtLib.Structures Require Import Functor Applicative.
 From ConCert.Execution.QCTests Require Import
   TestUtils ChainPrinters TraceGens TestContracts.
 From ConCert.Utils Require Import RecordUpdate.
+From ExtLib.Structures Require Monads.
 From Coq Require Import List.
 Import ListNotations.
 Import RecordSetNotations.
@@ -143,7 +144,7 @@ From ConCert.Execution.QCTests Require Import FA2Gens.
 
 
 Module TestInfo <: FA2TestsInfo.
-  From ExtLib.Structures Require Import Monads.
+  Import Monads.
   Import MonadNotation. Open Scope monad_scope.
 
   Definition fa2_contract_addr := token_contract_base_addr.

extraction/examples/ERC20LiquidityExtraction.v

@@ -18,13 +18,14 @@ From ConCert.Extraction Require Import
 From ConCert.Execution Require Import Automation.
 From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Import Blockchain.
-From ConCert.Execution Require Import EIP20Token.
+From ConCert.Execution Require EIP20Token.
+From ConCert.Execution Require Containers.
 From ConCert.Execution.Examples Require Import Common.
 From ConCert.Utils Require Import RecordUpdate.
 
 From Coq Require Import List Ascii String.
 Local Open Scope string_scope.
-
+From stdpp Require gmap.
 From MetaCoq.Template Require Import All.
 
 Import ListNotations.
@@ -78,8 +79,7 @@ Definition TT_remap_default : list (kername * string) :=
 Section EIP20TokenExtraction.
   Import EIP20Token.
   Import RecordSetNotations.
-  Require Import Containers.
-  From stdpp Require gmap.
+  Import Containers.
 
   Notation params := (ContractCallContext × option EIP20Token.Msg).
   Open Scope N_scope.

extraction/examples/EscrowExtract.v

@@ -16,6 +16,7 @@ From ConCert.Execution Require Import ResultMonad.
 From ConCert.Execution Require Import Serializable.
 From ConCert.Extraction Require Import Common Extraction.
 From ConCert.Extraction Require CameLIGOPretty CameLIGOExtract.
+From ConCert.Extraction Require LPretty LiquidityExtract.
 From ConCert.Utils Require Import RecordUpdate.
 
 From Coq Require Import List Ascii String.
@@ -115,7 +116,7 @@ End EscrowCameLIGOExtraction.
 Module EscrowLiquidityExtraction.
   Definition PREFIX := "".
 
-  From ConCert.Extraction Require Import LPretty LiquidityExtract.
+  Import LPretty LiquidityExtract.
   (** A translation table for definitions we want to remap. The corresponding top-level definitions will be *ignored* *)