Merge pull request #117 from ppedrot/case-pf-pose-dependent-metas

Adapt w.r.t. rocq-prover/rocq#17564.

Author: ppedrot

implementations/dyadics.v

@@ -182,7 +182,7 @@ Proof.
   repeat (split; try apply _).
    intros x y. unfold sg_op at 2, plus_is_sg_op, dy_plus.
    unfold equiv, dy_equiv, dy_inject, DtoQ_slow; simpl.
-   case (le_dec 0 0); intros E; simpl.
+   case (decide_rel); intros E; simpl.
     rewrite 2!rings.preserves_plus, ZtoQ_shift.
     rewrite rings.plus_negate_r.
     rewrite lattices.meet_l, int_pow_0. ring.
@@ -446,7 +446,7 @@ Section embed_rationals.
     intros x y E. rewrite <-E. clear y E.
     unfold DtoQ, DtoQ_slow.
     destruct x as [xm xe]. simpl.
-    case (decide_rel _); intros E.
+    case (decide_rel); intros E.
      now rewrite ZtoQ_shift.
     rewrite int_pow_negate_alt, ZtoQ_shift.
     now rewrite rings.preserves_1, left_identity.

implementations/field_of_fractions.v

@@ -115,10 +115,10 @@ Proof.
     rewrite 2!mult_1_r.
     apply (is_ne_0 1).
    unfold dec_recip, Frac_dec_recip.
-   case (decide_rel _); simpl; intuition.
+   case (decide_rel); simpl; intuition.
   intros [xn xs] Ex.
   unfold dec_recip, Frac_dec_recip.
-  case (decide_rel _); simpl.
+  simpl. case (decide_rel); simpl.
    intros E. destruct Ex. unfolds. rewrite E. ring.
   intros. ring_on_ring.
 Qed.
@@ -127,7 +127,7 @@ Lemma Frac_dec_mult_num_den x :
   x = 'num x / 'den x.
 Proof.
   unfold dec_recip, Frac_dec_recip.
-  case (decide_rel _); simpl; intros E.
+  simpl. case (decide_rel); simpl; intros E.
    now destruct (den_ne_0 x).
   unfolds. ring.
 Qed.

implementations/list_finite_set.v

@@ -245,14 +245,14 @@ Proof.
    intros E; split; revert E.
     induction l; simpl.
      intuition.
-    case (decide_rel _); intros ? E; intuition.
+    case (decide_rel); intros ? E; intuition.
     inversion_clear E; intuition.
    induction l; simpl.
     intros E1; inversion E1.
-   case (decide_rel _); intros ? E1; intuition.
+   case (decide_rel); intros ? E1; intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
   intros [E1 E2]. induction l; simpl; [easy|].
-  case (decide_rel _); intros E3.
+  case (decide_rel); intros E3.
    inversion_clear E1; intuition.
   inversion_clear E1 as [?? E4|]; intuition.
   destruct E3. now rewrite <-E4.
@@ -263,7 +263,7 @@ Lemma listset_meet_raw_NoDupA (l k : list A) :
 Proof.
   unfold meet. intros Pl. induction l; simpl; auto.
   inversion_clear Pl as [|? ? E1].
-  case (decide_rel _); intros; auto.
+  case (decide_rel); intros; auto.
   apply NoDupA_cons; auto.
   intros E2. destruct E1. now apply (listset_in_meet_raw l k _).
 Qed.
@@ -285,15 +285,15 @@ Proof.
    intros E; split; revert E.
     induction l; simpl.
      intuition.
-    case (decide_rel _); intros ? E; intuition.
+    case (decide_rel); intros ? E; intuition.
     inversion_clear E; intuition.
    induction l; simpl.
     intros E1; inversion E1.
-   case (decide_rel _); intros ? E1.
+   case (decide_rel); intros ? E1.
     intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
   intros [E1 E2]. induction l; simpl; [easy|].
-  case (decide_rel _); intros E3.
+  case (decide_rel); intros E3.
    inversion_clear E1 as [?? E4|]; intuition.
    destruct E2. now rewrite E4.
   inversion_clear E1; intuition.
@@ -304,7 +304,7 @@ Lemma listset_diff_raw_NoDupA (l k : list A) :
 Proof.
   unfold difference. intros Pl. induction l; simpl; auto.
   inversion_clear Pl as [|? ? E1].
-  case (decide_rel _); intros; auto.
+  case (decide_rel); intros; auto.
   apply NoDupA_cons; auto.
   intros E2. destruct E1. now apply (listset_in_diff_raw l k _).
 Qed.

implementations/nonneg_integers_naturals.v

@@ -75,11 +75,11 @@ Qed.
 Global Instance: CutMinusSpec (Z⁺) ZPos_cut_minus.
 Proof.
   split; intros [x Ex] [y Ey] E1; unfold cut_minus, ZPos_cut_minus; unfold_equivs.
-   case (decide_rel (≤)); intros E2.
+   case (decide_rel); intros E2.
     rewrite left_identity.
     now apply (antisymmetry (≤)).
    simpl. ring.
-  case (decide_rel (≤)); intros E2.
+  case (decide_rel); intros E2.
    reflexivity.
   simpl.
   apply (antisymmetry (≤)).

theory/int_pow.v

@@ -395,16 +395,16 @@ Section int_pow_default.
   Proof.
     split; unfold pow, int_pow_default.
        intros ? ? E1 ? ? E2.
-       now (case (decide_rel _); case (decide_rel _); rewrite E1, E2).
-      intros x. case (decide_rel _); intros E.
+       now (case (decide_rel); case (decide_rel); rewrite E1, E2).
+      intros x. case (decide_rel); intros E.
        now rewrite int_abs_0.
       now destruct E.
-     intros n ?. case (decide_rel _); intros E.
+     intros n ?. case (decide_rel); intros E.
       now apply nat_pow_base_0, int_abs_ne_0.
      rewrite nat_pow_base_0.
      apply dec_recip_0.
      now apply int_abs_ne_0.
-    intros x n E. case (decide_rel _); case (decide_rel _); intros E1 E2.
+    intros x n E. case (decide_rel); case (decide_rel); intros E1 E2.
        now rewrite int_abs_nonneg_plus, int_abs_1 by (auto;solve_propholds).
       setoid_replace n with (-1 : B).
        rewrite rings.plus_negate_r, int_abs_0, nat_pow_0.