Merge pull request #133 from jwiegley/johnw/silence

Construction/Coproduct.v

@@ -8,6 +8,8 @@ Section Coproduct.
 Context {C : Category}.
 Context {D : Category}.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Program Definition Coproduct : Category := {|
   obj     := C + D;
   hom     := fun x y =>

Construction/Free/Quiver.v

@@ -294,7 +294,10 @@ Proof.
   destruct p. reflexivity.
 Defined.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Local Notation "Q ⇨ Q'" := (QuiverHomomorphism Q Q') (at level 40).
+
 Definition QuiverComp {Q1 Q2 Q3: Quiver} (F : Q1 ⇨ Q2) (G : Q2 ⇨ Q3) : Q1 ⇨ Q3.
 Proof.
   unshelve refine

Instance/Adjoints.v

@@ -49,6 +49,8 @@ Record adj_morphism {C : Category} {D : Category} := {
   adjunction : free_functor ⊣ forgetful_functor
 }.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 #[export]
 Program Instance adj_morphism_setoid {C : Category} {D : Category} :
   Setoid (@adj_morphism C D) := {

Instance/Cat/Cartesian.v

@@ -8,6 +8,8 @@ Require Import Category.Instance.Cat.
 
 Generalizable All Variables.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 #[export]
 Program Instance Cat_Cartesian : @Cartesian Cat := {
   product_obj := @Product;

Instance/Lambda/Ltac.v

@@ -1,6 +1,8 @@
 Require Import Coq.Unicode.Utf8.
 Require Import Coq.Program.Program.
 
+Local Set Warnings "-deprecated-notation".
+
 Ltac reduce_jmeq :=
   repeat match goal with
   | [ H : ∀ _: _, _ ~= _ → _ |- _ ] =>

Instance/Lambda/Multi.v

@@ -73,6 +73,8 @@ Qed.
 
 #[local] Hint Extern 7 (_ ---> _) => repeat econstructor : core.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Corollary values_final {Γ τ} {e e' : Exp Γ τ} :
   e --->* e' → ValueP e → e = e'.
 Proof.

Instance/Parallel.v

@@ -62,6 +62,8 @@ Proof. inversion 1. Qed.
 
 Set Transparent Obligations.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Program Definition Parallel : Category := {|
   obj     := ParObj;
   hom     := fun x y => ∃ b : bool, ParHom b x y;

Instance/Rel.v

@@ -7,6 +7,8 @@ Require Import Coq.Sets.Ensembles.
 
 Generalizable All Variables.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 (* The category of heterogenous relations on Coq objects. *)
 
 Program Definition Rel : Category := {|

Instance/Sets/Cartesian/Closed.v

@@ -6,6 +6,8 @@ Require Import Category.Instance.Sets.Cartesian.
 
 Generalizable All Variables.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 (* This instance must appear in a separate file, because the Closed structure
    makes use of isomorphisms in [Sets]. *)
 

Instance/Two.v

@@ -28,6 +28,8 @@ Proof. inversion 1. Qed.
 
 #[export] Hint Extern 4 => contradiction TwoHom_Y_X_absurd : two_laws.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 (* The category 2 has two objects, their identity morphisms, and one morphism
    from the first object to the second (here denoted false and true). *)
 

Instance/Two/Discrete.v

@@ -32,6 +32,8 @@ Proof. inversion 1. Qed.
 
 #[export] Hint Extern 4 => contradiction TwoDHom_Y_X_absurd : two_laws.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 (* The discrete category 2 has two objects and their identity morphisms. *)
 
 Program Definition Two_Discrete : Category := {|

Lib/Datatypes.v

@@ -104,6 +104,8 @@ Proof.
   now apply IHxs.
 Qed.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 (* The only inductive types from the standard library used in this development
    are products and sums, so we must show how they interact with constructive
    setoids. *)

Lib/FMapExt.v

@@ -233,6 +233,8 @@ Proof.
   exact H2.
 Qed.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Lemma filter_add_true : ∀ elt k (e : elt) m m' P,
   Proper (E.eq ==> eq ==> eq) P
     → ~ M.In (elt:=elt) k m

Lib/MapDecide.v

@@ -56,6 +56,8 @@ Definition term_beq (x y : term) : bool :=
   | _, _ => false
   end.
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Lemma term_beq_sound x y : term_beq x y = true → x = y.
 Proof.
   induction x, y; simpl; intros; intuition.

Lib/Setoid.v

@@ -1,3 +1,5 @@
+Local Set Warnings "-notation-overridden". (* needed for Coq <8.16 *)
+
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Setoids.Setoid.
 Require Import Coq.Vectors.Fin.
@@ -66,9 +68,11 @@ Notation "∃! x .. y , P" := (Unique (fun x => .. (Unique (fun y => P)) ..))
   (at level 200, x binder, y binder, right associativity) : category_theory_scope.
 
 Local Set Warnings "-not-a-class".
+
 Class injective {A : Type} `{Setoid A} {B : Type} `{Setoid B} (f : A -> B) :=
-  { inj {x y} :> f x ≈ f y -> x ≈ y }.
+  { inj {x y} : f x ≈ f y -> x ≈ y }.
 
 Class surjective {A : Type} {B : Type} `{Setoid B} (f : A -> B) :=
-  { surj {y} :> { x & f x ≈ y} }.
+  { surj {y} : { x & f x ≈ y} }.
+
 Local Set Warnings "not-a-class".

Solver/Normal.v

@@ -51,6 +51,8 @@ Ltac solveit :=
   solve [ intros; subst; breakit; intuition; substituted
         | split; intros; breakit; intuition; discriminate ].
 
+Local Set Warnings "-intuition-auto-with-star".
+
 Program Fixpoint morphism_eq_dec (f g : Morphism) : {f = g} + {f ≠ g} :=
   match f, g with
   | Identity, Identity => left eq_refl