Fix warnings, imports

doc/equations_intro.v

@@ -16,7 +16,7 @@ From Equations.Prop Require Import Equations.
 
 (* begin hide *)
 Check @eq.
-Require Import Bvector.
+From Stdlib Require Import Bvector.
 
 (* Derive DependentElimination for nat bool option sum Datatypes.prod list *)
 (* end hide *)

dune-project

@@ -25,10 +25,14 @@
    (ppx_optcomp :build)
    (ocaml-lsp-server :with-dev-setup)))
 
+(package
+ (name rocq-equations-examples)
+ (synopsis "Examples")
+ (description "Do not install")
+ (depends rocq-equations))
+
 (package
  (name rocq-equations-tests)
  (synopsis "Technical package to run tests")
  (description "Do not install")
  (depends rocq-equations))
-
-(generate_opam_files)

examples/AlmostFull.v

@@ -1,17 +1,20 @@
 From Equations.Prop Require Import Equations.
 
 Require Import Examples.Fin.
-Require Import Relations Utf8.
-Require Import Relations Wellfounded.
-Require Import Setoid RelationClasses Morphisms.
-Require Import Lia.
-Require Import Bool.
-Require Import List Arith String.
+From Stdlib Require Import Relations Utf8.
+From Stdlib Require Import Relations Wellfounded.
+From Stdlib Require Import Setoid RelationClasses Morphisms.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List Arith String.
 From Stdlib Require Import FunctionalExtensionality.
 
 Set Equations Transparent.
 Set Keyed Unification.
 Set Asymmetric Patterns.
+Local Set Firstorder Solver auto with arith core datatypes.
+
+Ltac intuition_solver ::= auto with *.
 
 Section Equality.
   Class Eq (A : Type) :=
@@ -449,7 +452,7 @@ Section OplusUnary.
 
 End OplusUnary.
 
-Set Firstorder Solver auto.
+Local Set Firstorder Solver auto.
 
 (* Lemma oplus_unary_sec_intersection {X} (p q : WFT X) *)
 (*       (C : X -> X -> Prop) (A B : X -> Prop) : *)
@@ -610,7 +613,7 @@ Ltac destruct_pairs := repeat
   | [ x : _ /\ _ |- _ ] => destruct x
 end.
 
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Section SCT.
 
@@ -1353,7 +1356,7 @@ Print Assumptions size_change_wf.
 Print Assumptions size_change_termination.
 
 Definition R := product_rel Nat.le Nat.le.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Derive Signature for clos_trans_1n.
 
@@ -1391,7 +1394,7 @@ Definition gnlex : (nat * nat) -> nat.
   red. simpl. red. compute. simpl. intuition lia. red. simpl. compute. intuition lia.
 Defined.
 
-Require Import ExtrOcamlBasic.
+From Stdlib Require Import ExtrOcamlBasic.
 (* Extraction gnlex.
 Print Assumptions gnlex. *)
 

examples/Basics.v

@@ -22,9 +22,10 @@
   If running this interactively you can ignore the printing
   and hide directives which are just used to instruct coqdoc. *)
 
-Require Import Program Bvector List Relations.
+#[warnings="-deprecated-library-file-since-8.20"]
+From Stdlib Require Import Program Bvector List Relations.
 From Equations Require Import Equations Signature.
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 
 Set Keyed Unification.
 
@@ -65,7 +66,7 @@ app_with (cons a v) l with app_with v l => {
 (** Structurally recursive function on natural numbers, with inspection of a recursive
     call result. We use [auto with arith] to discharge the obligations. *)
 
-Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith.
+Local Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith.
 
 Equations equal (n m : nat) : { n = m } + { n <> m } :=
 equal O O := in_left ;
@@ -152,7 +153,7 @@ sublist p (cons x xs) with p x := {
 
 (** Well-founded definitions: *)
 
-Require Import Arith Wf_nat.
+From Stdlib Require Import Arith Wf_nat.
 
 (** One can declare new well-founded relations using instances of the [WellFounded] typeclass. *)
 #[local] Instance wf_nat : WellFounded lt := lt_wf.
@@ -230,6 +231,7 @@ Equations app {A} (l l' : list A) : list A :=
 app nil l := l;
 app (cons a v) l := cons a (app v l).
 
+#[warnings="-notation-overridden"]
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
 Equations rev_acc {A} (l : list A) (acc : list A) : list A :=
@@ -336,7 +338,8 @@ Qed.
 
 (* Eval compute in @zip''. *)
 
-Require Import Bvector.
+#[warnings="-deprecated-library-file-since-8.20"]
+From Stdlib Require Import Bvector.
 
 (** This function can also be defined by structural recursion on [m]. *)
 

examples/Equations_Tutorial_VeriMag.v

@@ -13,9 +13,10 @@
 (** printing <=? %$\le?$% *)
 (* begin hide *)
 
+Set Warnings "-undo-batch-mode".
 Set Warnings "-notation-overridden".
-Require Import Utf8 Arith Compare_dec List Lia.
-Require Import Relation_Operators Program.
+From Stdlib Require Import Utf8 Arith Compare_dec List Lia.
+From Stdlib Require Import Relation_Operators Program.
 
 Close Scope program_scope.
 Close Scope list_scope.
@@ -128,6 +129,7 @@ Module BuildingUp.
 (** Equations naturally supports notations: the left-hand 
   sides of clauses only have to be elaborated to well-typed patterns for the given argument types. *)
 
+Declare Scope mylist_scope.
 Notation "[]" := nil : mylist_scope.
 Notation "[ x ]" := (cons x nil) : mylist_scope.
 Notation "x :: l" := (cons x l) : mylist_scope.

examples/Fin.v

@@ -8,7 +8,7 @@
 
 (** An example development of the [fin] datatype using [equations]. *)
 
-From Coq.Program Require Import Basics Combinators.
+From Stdlib.Program Require Import Basics Combinators.
 From Equations.Prop Require Import Equations.
 Open Scope equations_scope.
 (** [fin n] is the type of naturals smaller than [n]. *)
@@ -78,7 +78,8 @@ Scheme finle_ind_dep := Induction for finle Sort Prop.
 
 Arguments finle {n}.
 
-Require Vectors.Vector.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Vectors.Vector.
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
 Notation vnil := Vector.nil.

examples/HoTT_light.v

@@ -11,9 +11,8 @@
  ** A lightweight version of the Homotopy Type Theory library prelude. *)
 Set Warnings "-notation-overridden".
 
-Require Export Unicode.Utf8.
-Require Import Stdlib.Program.Tactics Setoid.
-Require Import Relations.
+From Stdlib Require Export Unicode.Utf8.
+From Stdlib Require Import Program.Tactics Setoid Relations.
 (** Switches to constants in Type *)
 From Equations.Type Require Import All.
 
@@ -31,7 +30,7 @@ Set Implicit Arguments.
 (** Redefine a polymorphic identity function *)
 Definition id {A : Type} (a : A) : A := a.
 
-Require Import CRelationClasses CMorphisms.
+From Stdlib Require Import CRelationClasses CMorphisms.
 
 #[local] Instance id_reflexive A : Reflexive (@Id A).
 Proof. exact (@id_refl A). Defined.
@@ -67,7 +66,9 @@ Notation "p # x" := (transport _ p x) (right associativity, at level 65, only pa
 Notation "1" := id_refl : equations_scope.
 
 (** Notation for the inverse *)
-Reserved Notation "p ^" (at level 3, format "p '^'").
+#[warnings="-notation-incompatible-prefix"]
+Reserved Notation "p ^" (at level 1, format "p '^'").
+#[warnings="-notation-incompatible-prefix"]
 Notation "p ^" := (id_sym p%equations) : equations_scope.
 
 Equations apd {A} {B : A -> Type} (f : forall x : A, B x) {x y : A} (p : x = y) :

examples/MoreDep.v

@@ -3,7 +3,7 @@
   Porting a chapter of Adam Chlipala's Certified Programming with Dependent Types,
   #<a href="http://adam.chlipala.net/cpdt/html/MoreDep.html">More Dependent Types</a>#. *)
 
-Require Import Bool Arith List Program. 
+From Stdlib Require Import Bool Arith List Program. 
 From Equations.Prop Require Import Equations.
 Set Equations Transparent.
 
@@ -101,7 +101,7 @@ pairOut _ => None.
 
 Set Printing Depth 1000000.
 
-Require Import Wellfounded.
+From Stdlib Require Import Wellfounded.
 
 Equations cfold {t} (e : exp t) : exp t :=
 (* Works with well-foundedness too: cfold e by wf (signature_pack e) exp_subterm := *)
@@ -147,7 +147,7 @@ Inductive rbtree : color -> nat -> Set :=
 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
 Derive Signature NoConfusion for rbtree.
 
-Require Import Arith Lia.
+From Stdlib Require Import Arith Lia.
 
 Section depth.
   Variable f : nat -> nat -> nat.

examples/POPLMark1a.v

@@ -4,10 +4,10 @@
   inductive definition of scope and well-scoped variables (and terms,
   types and environments). *)
 
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import EquivDec.
-Require Import Arith.
+From Stdlib Require Import Arith.
 
 Definition scope := nat.
 Inductive var : scope -> Set :=

examples/RoseTree.v

@@ -6,12 +6,12 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 
-Require Import Utf8 Lia Arith.
+From Stdlib Require Import Utf8 Lia Arith.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Set Keyed Unification.

examples/STLC.v

@@ -14,12 +14,9 @@
   well-founded order on typable terms and conclude with a normalizer building
   beta-short eta-long normal forms, typable in a bidirectional type system. *)
 
-Require Program.
+From Stdlib Require Program.
 From Equations.Prop Require Import Equations.
-
-Require Import Lia.
-Require Import List Utf8.
-
+From Stdlib Require Import Lia List Utf8.
 Import ListNotations.
 
 Set Keyed Unification.
@@ -43,6 +40,7 @@ Delimit Scope term_scope with term.
 Bind Scope term_scope with term.
 
 Notation " @( f , x ) " := (App (f%term) (x%term)).
+#[warnings="-notation-incompatible-prefix"]
 Notation " 'λ' t " := (Lambda (t%term)) (at level 10).
 Notation " << t , u >> " := (Pair (t%term) (u%term)).
 
@@ -62,7 +60,7 @@ Coercion atom : atomic_type >-> type.
 Notation " x × y " := (product x y) (at level 90).
 Notation " x ---> y " := (arrow x y) (at level 30).
 
-Require Import Arith.
+From Stdlib Require Import Arith.
 
 Equations lift (k n : nat) (t : term) : term :=
 lift k n (Var i) with Nat.compare i k := {
@@ -104,7 +102,7 @@ Proof.
   funelim (lift k 0 t); term || rewrite ?H; crush.
 Qed.
 #[local] Hint Rewrite lift0 : lift.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Lemma lift_k_lift_k k n m t : lift k n (lift k m t) = lift k (n + m) t.
 Proof.
@@ -165,6 +163,7 @@ where "Γ |-- i : A " := (types Γ i A).
 
 Derive Signature for types.
 
+#[warnings="-notation-incompatible-prefix"]
 Notation " [ t ] u " := (subst 0 u t) (at level 10).
 
 Notation " x @ y " := (app x y) (at level 30, right associativity).
@@ -287,12 +286,12 @@ Inductive reduce : term -> term -> Prop :=
 where " t --> u " := (reduce t u). 
 Derive Signature for reduce.
 
-Require Import Relations.
+From Stdlib Require Import Relations.
 
 Definition reduces := clos_refl_trans term reduce.
 Notation " t -->* u " := (reduces t u) (at level 55).
 
-Require Import Setoid.
+From Stdlib Require Import Setoid.
 
 #[local]
 Instance: Transitive reduces.
@@ -545,7 +544,7 @@ Proof. intros. now apply eta_expand in H0; term. Qed.
 
 (** Going to use the subterm order *)
 
-Require Import Arith Wf_nat.
+From Stdlib Require Import Arith Wf_nat.
 #[export] Instance wf_nat : Classes.WellFounded lt := lt_wf.
 
 #[local] Hint Constructors Subterm.lexprod : subterm_relation.
@@ -721,7 +720,7 @@ Proof.
   (* Lt *)
   apply Nat.compare_lt_iff in Heq. depelim H0.
   replace (nth i (Γ' @ (_ :: Γ)) unit) with (nth i (Γ' @ Γ) unit).
-  constructor. rewrite app_length. auto with arith.
+  constructor. rewrite length_app. auto with arith.
   now do 2 rewrite <- nth_extend_right by auto. 
 
   (* Gt *)
@@ -784,7 +783,7 @@ Proof.
     intros Ht2; subst t. simpl in *. depelim H0.
     specialize (Hind _ _ H H0); eauto. now apply pair_elim_snd with A0.
 Qed.
-Print Assumptions hereditary_subst_type.
+(* Print Assumptions hereditary_subst_type. *)
 Import Program.Basics.
 #[export] Instance: subrelation eq (flip impl).
 Proof. reduce. subst; auto. Qed.
@@ -856,18 +855,18 @@ Proof.
     split; intros Hsyn; depelim Hsyn;
     [depelim H1;constructor;auto|];
     (rewrite nth_app_l by lia; rewrite <- nth_app_l with (l':=Γ) by lia;
-     constructor; rewrite app_length; auto with arith). 
+     constructor; rewrite length_app; auto with arith). 
 
   (* Gt *)
   - apply Nat.compare_gt_iff in Heq.
     split; intros Hsyn; depelim Hsyn.
     depelim H1. constructor. auto.
     replace (nth i (Γ' @ (A :: Γ)) unit) with (nth (pred i) (Γ' @ Γ) unit).
-    constructor. rewrite app_length in *. simpl in H1. lia.
+    constructor. rewrite length_app in *. simpl in H1. lia.
     now apply nth_pred.
 
     replace (nth _ (Γ' @ (_ :: _)) unit) with (nth (pred i) (Γ' @ Γ) unit).
-    constructor. rewrite app_length in *. simpl in H0. lia.
+    constructor. rewrite length_app in *. simpl in H0. lia.
     now apply nth_pred.
 
   (* App *)
@@ -1003,7 +1002,7 @@ Proof.
     split; auto. intros H1. depelim H1. term. 
 Qed.
 
-Print Assumptions hereditary_subst_subst.
+(* Print Assumptions hereditary_subst_subst. *)
 
 Lemma check_liftn {Γ Γ' t T} : Γ |-- t <= T -> Γ' @ Γ |-- lift 0 (length Γ') t <= T.
 Proof. intros. apply (check_lift Γ t T [] H Γ'). Qed.
@@ -1054,4 +1053,4 @@ Proof. induction 1. (* eta-exp *)
   depelim H0.
 Qed.
 
-Print Assumptions types_normalizes.
+(* Print Assumptions types_normalizes. *)