Merge pull request #225 from mrhaandi/some-8.20-warnings

dealt with some 8.20 warnings

theories/FOL/TRAKHTENBROT/Sig2_Sign.v

@@ -52,7 +52,7 @@ Section Sig2_Sig_n_encoding.
     Variable (X : Type) (M2 : fo_model Σ2 X) (Mn : fo_model Σn X).
 
     Notation "⟪ A ⟫" := (fun ψ => fol_sem M2 ψ A).
-    Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'").
+    Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'").
 
     Let P2 a b := fom_rels M2 tt (a##b##ø).
     Let Pn a b := fom_rels Mn tt (a##vec_set_pos (fun _ => b)).

theories/FOL/TRAKHTENBROT/Sig_one_rel.v

@@ -30,7 +30,7 @@ Set Implicit Arguments.
 
 (* * From several relations to one, arity incremented by 1 *)
 
-Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'").
+Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'").
 
 Local Notation ø := vec_nil.
 

theories/FOL/TRAKHTENBROT/Sig_rem_cst.v

@@ -24,7 +24,7 @@ Set Implicit Arguments.
 
 (* * From signatures with only constants functions to function symbol free signatures *)
 
-Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'").
+Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'").
 
 Local Notation ø := vec_nil.
 

theories/FOL/TRAKHTENBROT/Sig_rem_props.v

@@ -24,7 +24,7 @@ Set Implicit Arguments.
 
 (* * Removing constant propositions from monadic signatures *)
 
-Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'").
+Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'").
 
 Local Notation ø := vec_nil.
 

theories/FOL/TRAKHTENBROT/Sign_Sig.v

@@ -53,7 +53,7 @@ Section Sig_n_Sig.
     Defined.
 
     Notation "⟪ A ⟫" := (fun ψ => fol_sem M ψ A).
-    Notation "⟪ A ⟫'" := (fun φ => fol_sem M_enc_n φ A) (at level 1, format "⟪ A ⟫'").
+    Notation "⟪ A ⟫'" := (fun φ => fol_sem M_enc_n φ A) (at level 0, format "⟪ A ⟫'").
 
     Local Fact enc_correct_1 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ.
     Proof.
@@ -96,7 +96,7 @@ Section Sig_n_Sig.
     Defined. 
 
     Notation "⟪ A ⟫" := (fun ψ => fol_sem Mn_enc ψ A).
-    Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'").
+    Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'").
 
     Local Fact enc_correct_2 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ.
     Proof.

theories/FOL/TRAKHTENBROT/Sign_Sig2.v

@@ -86,7 +86,7 @@ Section Sign_Sig2_encoding.
          -> P v <-> mb_is_tuple_in (fun a b => a ∈ₘ b) r w.
 
   Notation "⟪ A ⟫" := (fun ψ => fol_sem M2 ψ A).
-  Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'").
+  Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'").
 
   (* The correctness lemma *)
 

theories/FOL/TRAKHTENBROT/btree.v

@@ -934,7 +934,7 @@ Proof. intros ? ? H; apply bte_ext; intro; do 2 rewrite bt_pow_spec; rewrite H;
 
 Definition bt_opair s t := (s⪧∅)⪧(s⪧t⪧∅)⪧∅.
 
-Local Notation "⟬ s , t ⟭" := (bt_opair s t) (at level 1, format "⟬ s , t ⟭").
+Local Notation "⟬ s , t ⟭" := (bt_opair s t) (at level 0, format "⟬ s , t ⟭").
 
 Section ordered_pairs.
 

theories/FOL/TRAKHTENBROT/fo_logic.v

@@ -606,10 +606,10 @@ Section fo_model_simulation.
   Infix "⋈" := R (at level 70, no associativity).
 
   Notation "⟦ t ⟧" := (fun φ => fo_term_sem M φ t).
-  Notation "⟦ t ⟧'" := (fun φ => fo_term_sem N φ t) (at level 1, format "⟦ t ⟧'").
+  Notation "⟦ t ⟧'" := (fun φ => fo_term_sem N φ t) (at level 0, format "⟦ t ⟧'").
 
   Notation "⟪ A ⟫" := (fun φ => fol_sem M φ A).
-  Notation "⟪ A ⟫'" := (fun φ => fol_sem N φ A) (at level 1, format "⟪ A ⟫'").
+  Notation "⟪ A ⟫'" := (fun φ => fol_sem N φ A) (at level 0, format "⟪ A ⟫'").
 
   (* The simulation lifts from variables to terms *)
 

theories/FOL/TRAKHTENBROT/membership.v

@@ -98,9 +98,9 @@ Section membership.
     + rewrite H1, H2; auto.
   Qed.
 
-  Reserved Notation "p ≋ ⦃ a , b ⦄" (at level 70, format "p  ≋  ⦃ a , b ⦄").
-  Reserved Notation "p ≋ ⦅ a , b ⦆" (at level 70, format "p  ≋  ⦅ a , b ⦆").
-  Reserved Notation "t ≋ ⦉ v ⦊" (at level 70, format "t  ≋  ⦉ v ⦊").
+  Reserved Notation "p ≋ ⦃ a , b ⦄" (at level 1, format "p  ≋  ⦃ a , b ⦄").
+  Reserved Notation "p ≋ ⦅ a , b ⦆" (at level 1, format "p  ≋  ⦅ a , b ⦆").
+  Reserved Notation "t ≋ ⦉ v ⦊" (at level 1, format "t  ≋  ⦉ v ⦊").
 
   Definition mb_is_pair p x y := forall a, a ∈ p <-> a ≈ x \/ a ≈ y.
 

theories/FOL/TRAKHTENBROT/notations.v

@@ -74,15 +74,15 @@ Reserved Notation "⇡ sig" (at level 1, format "⇡ sig").
 
 (* Term substitution and semantics *)
 Reserved Notation "t '⟬' σ '⟭'" (at level 1, format "t ⟬ σ ⟭").
-Reserved Notation "'⟦' t '⟧'" (at level 1, format "⟦ t ⟧").
+Reserved Notation "'⟦' t '⟧'" (at level 0, format "⟦ t ⟧").
 
 (* Formula subsitution and semantics*)
 Reserved Notation "f '⦃' σ '⦄'" (at level 1, format "f ⦃ σ ⦄").
-Reserved Notation "'⟪' f '⟫'" (at level 1, format "⟪ f ⟫").
+Reserved Notation "'⟪' f '⟫'" (at level 0, format "⟪ f ⟫").
 
 (* Unary ops *)
 
-Reserved Notation "⌞ x ⌟" (at level 1, format "⌞ x ⌟").
+Reserved Notation "⌞ x ⌟" (at level 0, format "⌞ x ⌟").
 Reserved Notation "↓ x"   (at level 1, format "↓ x").
 Reserved Notation "x †"   (at level 1, format "x †").
 
@@ -92,7 +92,7 @@ Reserved Notation "x ∙ y"  (at level 2, right associativity, format "x ∙ y")
 Reserved Notation "x ⪧ y" (at level 2, right associativity, format "x ⪧ y").
 Reserved Notation "x → y" (at level 2, right associativity, format "x → y").
 
-Reserved Notation "⟬ s , t ⟭" (at level 1, format "⟬ s , t ⟭").
+Reserved Notation "⟬ s , t ⟭" (at level 0, format "⟬ s , t ⟭").
 Reserved Notation "x ∪ y" (at level 52, left associativity).
 
 (* Infix Binary rels *)

theories/L/Prelim/ARS.v

@@ -106,7 +106,8 @@ Section FixX.
   Lemma ecl_sym R :
     symmetric (ecl R).
   Proof.
-    induction 1; eauto using ecl, (@ecl_trans R).
+    pose proof (@ecl_trans R).
+    induction 1; eauto using ecl.
   Qed.
 
   Lemma star_ecl R :
@@ -164,7 +165,9 @@ Section FixX.
       + exists y. eauto using star.
                + destruct (A _ _ _ D B) as [v [E F]].
                  destruct (IH _ E) as [u [G H]].
-                 exists u. eauto using (@star_trans R).
+                 exists u.
+                 pose proof (@star_trans R).
+                 eauto.
                - apply (A x y z); eauto using star.
   Qed.
 
@@ -179,14 +182,16 @@ Section FixX.
   Proof.
     split; intros A.
     - intros x y z B C. apply A.
-      eauto using (@ecl_trans R), star_ecl, (@ecl_sym R).
+      pose proof (@ecl_trans R).
+      pose proof (@ecl_sym R).
+      eauto using star_ecl.
     - intros x y B. apply semi_confluent_confluent in A.
       induction B as [x|x x' y C B IH|x x' y C B IH].
       + exists x. eauto using star.
                + destruct IH as [z [D E]]. exists z. eauto using star.
                + destruct IH as [u [D E]].
                  destruct (A _ _ _ C D) as [z [F G]].
-                 exists z. eauto using (@star_trans R).
+                 exists z. pose proof (@star_trans R). eauto.
   Qed.
 
 

theories/StringRewriting/Reductions/SBTM_HALT_to_SR.v

@@ -85,14 +85,21 @@ Section Construction.
   Lemma In_srsI u v : In (u, v) srs -> In_srs u v.
   Proof.
     move=> /in_flat_map [[q a]] [_] /=.
+    have ? := In_srs_l2 _ true.
+    have ? := In_srs_l2 _ false.
+    have ? := In_srs_r2 _ true.
+    have ? := In_srs_r2 _ false.
+    have ? := In_srs_dl _ true.
+    have ? := In_srs_dl _ false.
+    have ? := In_srs_dr _ true.
+    have ? := In_srs_dr _ false.
     case E: (trans' M (q, a)) => [[[q' a'] []]|] /=.
     - move=> [|[|[|[]]]] => - [<- <-].
-      all: by auto using In_srs_l1, (In_srs_l2 _ true), (In_srs_l2 _ false).
+      all: by auto using In_srs_l1.
     - move=> [|[|[|[]]]] => - [<- <-].
-      all: by auto using In_srs_r1, (In_srs_r2 _ true), (In_srs_r2 _ false).
+      all: by auto using In_srs_r1.
     - move=> [|[|[|[|[|[]]]]]] => - [<- <-].
-      all: by auto using In_srs_f, (In_srs_dl _ true), (In_srs_dl _ false),
-        (In_srs_dr _ true), (In_srs_dr _ false).
+      all: by auto using In_srs_f.
   Qed.
 
   (* step simulation *)

theories/_CoqProject

@@ -1,6 +1,6 @@
 -Q . Undecidability
 
--arg -w -arg -notation-overridden,-stdlib-vector
+-arg -w -arg -notation-overridden,-stdlib-vector,-notation-incompatible-prefix
 -arg "-set" -arg "'Default Proof Using = Type'"
 COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html --with-footer ../website/resources/footer.html --index indexpage"