Fix warnings

embedding/_CoqProject

@@ -1,4 +1,3 @@
--arg -w -arg -undeclared-scope
 -arg -w -arg -notation-overridden
 -arg -w -arg -non-reversible-notation
 

embedding/examples/AcornExamples.v

@@ -200,6 +200,7 @@ Definition Functions := [("singleton", eTyLam "A" (eLambda "x" (tyRel 0) (eApp (
     now f_equal.
   Qed.
 
+  #[local]
   Hint Rewrite acorn_foldr_coq_fold_right concat_app from_to_acorn : hints.
 
   Lemma concat_assoc :
@@ -366,16 +367,21 @@ Module Recursion.
   Lemma Nat_nat_right n : Nat_nat (nat_Nat n) = n.
   Proof. induction n;simpl;f_equal;auto. Qed.
 
+  #[local]
   Hint Resolve Nat_nat_left Nat_nat_right : hints.
-
-  Local Coercion Nat_nat : Nat >-> nat.
-  Local Coercion nat_Nat : nat >-> Nat.
+
+  #[local]
+  Set Warnings "-ambiguous-paths".
+
+  #[local]
+  Coercion Nat_nat : Nat >-> nat.
+  #[local]
+  Coercion nat_Nat : nat >-> Nat.
 
   Lemma add_correct (n m : Nat) :
   add n m = n + m.
   Proof. induction n;simpl;f_equal;auto with hints. Qed.
 
-
 End Recursion.
 
 

embedding/extraction/PreludeExt.v

@@ -9,6 +9,7 @@ From ConCert.Embedding Require Import TranslationUtils.
 From ConCert.Embedding Require Import Prelude.
 From ConCert.Embedding Require Import Utils.
 From ConCert.Execution Require Import Blockchain.
+From ConCert.Execution Require Import Serializable.
 From ConCert.Utils Require Import Automation.
 From Coq Require Import String.
 From Coq Require Import ZArith.

embedding/theories/EnvSubst.v

@@ -43,7 +43,7 @@ Module NamelessSubst.
       end.
 
 
-   (** NOTE: assumes, that expression in [ρ] are closed! *)
+  (** NOTE: assumes, that expression in [ρ] are closed! *)
   Fixpoint subst_env_i_aux (k : nat) (ρ : env expr) (e : expr) : expr :=
     match e with
     | eRel i => if Nat.leb k i then
@@ -225,6 +225,7 @@ Module Equivalence.
    Definition list_val_equiv vs1 vs2 := Forall2 (fun v1 v2 => v1 ≈ v2) vs1 vs2.
    Notation " vs1 ≈ₗ vs2 " := (list_val_equiv vs1 vs2) (at level 50).
 
+   #[export]
    Instance val_equiv_reflexive : Reflexive val_equiv.
    Proof.
      intros v. induction v using val_ind_full.
@@ -239,16 +240,21 @@ Module Equivalence.
    Axiom val_equiv_symmetric : Symmetric val_equiv.
    Axiom val_equiv_transitive : Transitive val_equiv.
 
+   #[export]
    Existing Instance val_equiv_symmetric.
+   #[export]
    Existing Instance val_equiv_transitive.
 
    (* TODO:  Define these  *)
    Axiom list_val_equiv_reflexive : Reflexive list_val_equiv.
    Axiom list_val_equiv_symmetric : Symmetric list_val_equiv.
    Axiom list_val_equiv_transitive : Transitive list_val_equiv.
 
+   #[export]
    Existing Instance list_val_equiv_reflexive.
+   #[export]
    Existing Instance list_val_equiv_symmetric.
+   #[export]
    Existing Instance list_val_equiv_transitive.
 
    Lemma list_val_compat v1 v2 vs1 vs2 :
@@ -258,6 +264,7 @@ Module Equivalence.
      constructor;easy.
    Qed.
 
+   #[export]
    Instance cons_compat : Proper (val_equiv ==> list_val_equiv ==> list_val_equiv) cons.
    Proof.
       cbv;intros;apply list_val_compat;assumption.
@@ -273,6 +280,7 @@ Module Equivalence.
       + constructor; assumption.
     Defined.
 
+    #[export]
     Instance constr_morph i nm : Proper (list_val_equiv ==> val_equiv) (vConstr i nm).
     Proof.
       cbv;intros;apply constr_cons_compat;assumption.

embedding/theories/pcuic/PCUICCorrectness.v

@@ -30,9 +30,9 @@ Local Set Keyed Unification.
 Open Scope nat.
 
 #[local]
- Hint Resolve assumption_context_subst
-              assumption_context_map_vass
-              PCUICSigmaCalculus.context_assumptions_context : hints.
+Hint Resolve assumption_context_subst
+             assumption_context_map_vass
+             PCUICSigmaCalculus.context_assumptions_context : hints.
 
 (** Soundness (In the paper: Theorem 1) *)
 Theorem expr_to_term_sound (n : nat) (ρ : env val) Σ1 Σ2

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -729,8 +729,8 @@ Qed.
 #[export] Hint Constructors val_ok Forall : hints.
 #[export] Hint Unfold snd env_ok AllEnv compose : hints.
 
-#[export] Hint Resolve 1 subst_env_iclosed_n_inv subst_env_iclosed_0_inv: hints.
-#[export] Hint Resolve 1 subst_env_iclosed_n subst_env_iclosed_0 : hints.
+#[export] Hint Resolve subst_env_iclosed_n_inv subst_env_iclosed_0_inv: hints.
+#[export] Hint Resolve subst_env_iclosed_n subst_env_iclosed_0 : hints.
 
 Lemma option_to_res_ok {A} (o : option A) s v:
   option_to_res o s = Ok v ->
@@ -1129,8 +1129,8 @@ Proof.
   symmetry. eapply subst_env_swap_app;eauto.
 Qed.
 
-Remove Hints iclosed_n_geq: hints.
-Remove Hints Bool.absurd_eq_true : core.
+#[local] Remove Hints iclosed_n_geq: hints.
+#[local] Remove Hints Bool.absurd_eq_true : core.
 
 Open Scope nat.
 
@@ -1166,9 +1166,9 @@ Qed.
 #[export] Hint Resolve ty_env_ok_app_rec : hints.
 #[export] Hint Resolve subst_env_compose_1 : hints.
 
-Hint Extern 2 (iclosed_n _ (snd _) = _) => simpl : hints.
-Hint Extern 2 (_ .[_] = _)=> simpl;eapply subst_env_compose_1 with (k:=0) : hints.
-Hint Extern 2 (iclosed_n ?n _ = _)=> (match n with
+#[export] Hint Extern 2 (iclosed_n _ (snd _) = _) => simpl : hints.
+#[export] Hint Extern 2 (_ .[_] = _)=> simpl;eapply subst_env_compose_1 with (k:=0) : hints.
+#[export] Hint Extern 2 (iclosed_n ?n _ = _)=> (match n with
                                     | O => fail
                                     | S _ => eapply iclosed_n_0
                                      end) : hints.
@@ -1895,10 +1895,10 @@ Proof.
   intros. now apply closed_exprs_len_iff.
 Qed.
 
-#[export] Hint Resolve 0 closed_exprs_len_r2l : hints.
+#[export] Hint Resolve closed_exprs_len_r2l : hints.
 
-Hint Extern 1 (iclosed_n (#|_|) _ = _) =>
-eapply closed_exprs_len_iff with (n:=0) : hints.
+#[export] Hint Extern 1 (iclosed_n (#|_|) _ = _) =>
+  eapply closed_exprs_len_iff with (n:=0) : hints.
 
 Definition not_stuck : term -> bool :=
   fun t => let (f, args) := decompose_app t in

embedding/theories/pcuic/PCUICFacts.v

@@ -22,6 +22,7 @@ Open Scope string_scope.
 Import ListNotations.
 Import NamelessSubst.
 
+#[export]
 Hint Unfold expr_eval_n expr_eval_i : facts.
 
 (** An elimination principle that takes into account nested occurrences of expressions
@@ -416,7 +417,7 @@ Section Values.
     + simpl.
       inversion Hv. subst.
       eauto with facts.
-Qed.
+  Qed.
 
 
   Lemma subst_env_i_ty_empty k t : t = subst_env_i_ty k [] t.

examples/_CoqProject

@@ -1,3 +1,6 @@
+-arg -w -arg -notation-overridden
+-arg -w -arg -non-reversible-notation
+
 -R ../utils/theories ConCert.Utils
 -R ../execution/theories ConCert.Execution
 -R ../execution/test ConCert.Execution.Test

examples/bat/BAT.v

@@ -16,6 +16,7 @@ From ConCert.Utils Require Import RecordUpdate.
 From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import Containers.
 From ConCert.Execution Require Import Monad.
+From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Import ResultMonad.
 From ConCert.Execution Require Import ContractCommon.
 From ConCert.Examples.BAT Require Import BATCommon.

examples/bat/BATAltFix.v

@@ -17,6 +17,7 @@ From ConCert.Utils Require Import RecordUpdate.
 From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import Containers.
 From ConCert.Execution Require Import Monad.
+From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Import ResultMonad.
 From ConCert.Execution Require Import ContractCommon.
 From ConCert.Examples.BAT Require Import BATCommon.

examples/bat/BATAltFixTests.v

@@ -7,7 +7,7 @@ From ConCert.Execution.Test Require Import QCTest.
 From ConCert.Examples.BAT Require Import BATCommon.
 From ConCert.Examples.BAT Require Import BATAltFix.
 From ConCert.Examples.BAT Require Import BATGens.
-From ConCert.Examples.BAT Require Import BATPrinters.
+From ConCert.Examples.BAT Require Export BATPrinters.
 From ConCert.Examples.BAT Require Import BATTestCommon.
 From Coq Require Import List.
 From Coq Require Import ZArith_base.

examples/bat/BATFixed.v

@@ -17,6 +17,7 @@ From ConCert.Utils Require Import RecordUpdate.
 From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import Containers.
 From ConCert.Execution Require Import Monad.
+From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Import ResultMonad.
 From ConCert.Execution Require Import ContractCommon.
 From ConCert.Examples.BAT Require Import BATCommon.

examples/bat/BATFixedTests.v

@@ -7,7 +7,7 @@ From ConCert.Execution.Test Require Import QCTest.
 From ConCert.Examples.BAT Require Import BATCommon.
 From ConCert.Examples.BAT Require Import BATFixed.
 From ConCert.Examples.BAT Require Import BATGens.
-From ConCert.Examples.BAT Require Import BATPrinters.
+From ConCert.Examples.BAT Require Export BATPrinters.
 From ConCert.Examples.BAT Require Import BATTestCommon.
 From Coq Require Import List.
 From Coq Require Import ZArith_base.

examples/bat/BATPrinters.v

@@ -6,11 +6,13 @@ From ConCert.Examples.EIP20 Require Import EIP20TokenPrinters.
 
 Local Open Scope string_scope.
 
+#[export]
 Instance showTokenValue : Show TokenValue :=
 {|
   show v := show v
 |}.
 
+#[export]
 Instance showMsg : Show BATCommon.Msg :=
 {|
   show m := match m with
@@ -21,6 +23,7 @@ Instance showMsg : Show BATCommon.Msg :=
             end
 |}.
 
+#[export]
 Instance showBATSetup : Show BATCommon.Setup :=
 {|
   show setup := "Setup{" ++
@@ -34,6 +37,7 @@ Instance showBATSetup : Show BATCommon.Setup :=
     "tokenCreationMin: " ++ show setup.(_tokenCreationMin) ++ "}"
 |}.
 
+#[export]
 Instance showBATState : Show BATCommon.State :=
 {|
   show s := "State{" ++
@@ -49,5 +53,6 @@ Instance showBATState : Show BATCommon.State :=
     "tokenCreationMin: " ++ show s.(tokenCreationMin) ++ "}"
 |}.
 
+#[export]
 Instance showSerializedMsg : Show SerializedValue :=
   Derive Show Msg < BATCommon.Msg, BATCommon.Setup >.

examples/bat/BATTests.v

@@ -7,7 +7,7 @@ From ConCert.Execution.Test Require Import QCTest.
 From ConCert.Examples.BAT Require Import BATCommon.
 From ConCert.Examples.BAT Require Import BAT.
 From ConCert.Examples.BAT Require Import BATGens.
-From ConCert.Examples.BAT Require Import BATPrinters.
+From ConCert.Examples.BAT Require Export BATPrinters.
 From ConCert.Examples.BAT Require Import BATTestCommon.
 From Coq Require Import List.
 From Coq Require Import ZArith_base.