Making those proofs which depend on names generated for the arguments

in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.

3 files changed, 10 insertions, 10 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index 7a92ff0c0..98e0c29c7 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -328,7 +328,7 @@ Section DoubleMul.
    rewrite <- (Z.add_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith.
    simpl ww_to_Z in H1. assert (U:=spec_to_Z cch).
    assert ([|wc|]*wB + [|cch|] <= 2*wB - 3).
-    destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3));trivial.
+    destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3)) as [Hle|Hgt];trivial.
     assert ([|xh|] * [|yl|] + [|xl|] * [|yh|] <= (2*wB - 4)*wB + 2).
      ring_simplify ((2*wB - 4)*wB + 2).
      assert (H4 := Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)).
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 52ae56e2b..1be361b66 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -635,7 +635,7 @@ Section Basics.
    EqShiftL k x y  <-> firstn (size-k) (i2l x) = firstn (size-k) (i2l y).
  Proof.
  intros.
- destruct (le_lt_dec size k).
+ destruct (le_lt_dec size k) as [Hle|Hlt].
  split; intros.
  replace (size-k)%nat with O by omega.
  unfold firstn; auto.
@@ -661,7 +661,7 @@ Section Basics.
   EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y.
  Proof.
  intros.
- destruct (le_lt_dec size k).
+ destruct (le_lt_dec size k) as [Hle|Hlt].
  split; intros; apply EqShiftL_size; auto.
 
  rewrite 2 EqShiftL_i2l.
@@ -684,7 +684,7 @@ Section Basics.
   EqShiftL (S k) (shiftr x) (shiftr y).
  Proof.
  intros.
- destruct (le_lt_dec size (S k)).
+ destruct (le_lt_dec size (S k)) as [Hle|Hlt].
  apply EqShiftL_size; auto.
  case_eq (firstr x); intros.
  rewrite <- EqShiftL_twice.
@@ -884,18 +884,18 @@ Section Basics.
  specialize IHn with p.
  destruct (p2ibis n p). simpl @snd in *.
  rewrite nshiftr_S_tail.
- destruct (le_lt_dec size n).
+ destruct (le_lt_dec size n) as [Hle|Hlt].
  rewrite nshiftr_above_size; auto.
- assert (H:=nshiftr_0_firstl _ _ l IHn).
+ assert (H:=nshiftr_0_firstl _ _ Hlt IHn).
  replace (shiftr (twice_plus_one i)) with i; auto.
  destruct i; simpl in *. rewrite H; auto.
 
  specialize IHn with p.
  destruct (p2ibis n p); simpl @snd in *.
  rewrite nshiftr_S_tail.
- destruct (le_lt_dec size n).
+ destruct (le_lt_dec size n) as [Hle|Hlt].
  rewrite nshiftr_above_size; auto.
- assert (H:=nshiftr_0_firstl _ _ l IHn).
+ assert (H:=nshiftr_0_firstl _ _ Hlt IHn).
  replace (shiftr (twice i)) with i; auto.
  destruct i; simpl in *; rewrite H; auto.
 
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 334836954..dbc7582d5 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -466,8 +466,8 @@ Section ZModulo.
  generalize (Zgcd_is_gcd a b); inversion_clear 1.
  destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4.
  assert (H4:=Z.gcd_nonneg a b).
- destruct (Z.eq_dec (Z.gcd a b) 0).
- rewrite e; generalize (Zmax_spec a b); omega.
+ destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq].
+ generalize (Zmax_spec a b); omega.
  assert (0 <= q).
   apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith.
  destruct (Z.eq_dec q 0).