Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.

10 files changed, 156 insertions, 173 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 7e8a1018..5b5d37ee 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -56,8 +56,6 @@ module P = struct
   let one = Coq_xH
   let succ = Pos.succ
   let pred = Pos.pred
-  let add = Pos.add
-  let sub = Pos.sub
   let eq x y = (Pos.compare x y = Eq)
   let lt x y = (Pos.compare x y = Lt)
   let gt x y = (Pos.compare x y = Gt)
@@ -106,8 +104,6 @@ module P = struct
       then Coq_xH
       else Coq_xI (of_int64 (Int64.shift_right_logical n 1))
 
-  let (+) = add
-  let (-) = sub
   let (=) = eq
   let (<) = lt
   let (<=) = le
@@ -124,11 +120,6 @@ module N = struct
 
   let zero = N0
   let one = Npos Coq_xH
-  let succ = N.succ
-  let pred = N.pred
-  let add = N.add
-  let sub = N.sub
-  let mul = N.mul
   let eq x y = (N.compare x y = Eq)
   let lt x y = (N.compare x y = Lt)
   let gt x y = (N.compare x y = Gt)
@@ -157,9 +148,6 @@ module N = struct
   let of_int64 n =
     if n = 0L then N0 else Npos (P.of_int64 n)
 
-  let (+) = add
-  let (-) = sub
-  let ( * ) = mul
   let (=) = eq
   let (<) = lt
   let (<=) = le
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index fc4a59f6..6fa82492 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -22,6 +22,8 @@ Require Export Znumtheory.
 Require Export List.
 Require Export Bool.
 
+Global Set Asymmetric Patterns.
+
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
@@ -768,7 +770,7 @@ Proof.
   discriminate.
   rewrite list_length_z_cons. destruct (zeq n 0).
   generalize (list_length_z_pos l); omega.
-  exploit IHl; eauto. unfold Zpred. omega.
+  exploit IHl; eauto. omega.
 Qed.
 
 (** Properties of [List.incl] (list inclusion). *)
@@ -1431,4 +1433,3 @@ Lemma nlist_forall2_imply:
 Proof.
   induction 1; simpl; intros; constructor; auto.
 Qed.
-
diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v
index fe7f7c6d..f5ccec2a 100644
--- a/lib/Fappli_IEEE_extra.v
+++ b/lib/Fappli_IEEE_extra.v
@@ -63,10 +63,10 @@ Qed.
 
 Definition is_finite_pos0 (f: binary_float) : bool :=
   match f with
-  | B754_zero s => negb s
-  | B754_infinity _ => false
-  | B754_nan _ _ => false
-  | B754_finite _ _ _ _ => true
+  | B754_zero _ _ s => negb s
+  | B754_infinity _ _ _ => false
+  | B754_nan _ _ _ _ => false
+  | B754_finite _ _ _ _ _ _ => true
   end.
 
 Lemma Bsign_pos0:
@@ -693,10 +693,10 @@ Qed.
 
 Definition ZofB (f: binary_float): option Z :=
   match f with
-    | B754_finite s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z
-    | B754_finite s m 0 _ => Some (cond_Zopp s (Zpos m))
-    | B754_finite s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z
-    | B754_zero _ => Some 0%Z
+    | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z
+    | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m))
+    | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z
+    | B754_zero _ _ _ => Some 0%Z
     | _ => None
   end.
 
@@ -949,7 +949,9 @@ Proof.
 - revert H H0. fold emin. fold fexp.
   set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x).
   set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y).
-  rewrite (Rmult_comm ry rx). destruct Rlt_bool.
+  rewrite (Rmult_comm ry rx).
+  destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode) (rx * ry)))
+                     (bpow radix2 emax)).
   + intros (A1 & A2 & A3) (B1 & B2 & B3).
     apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto.
     rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm.
@@ -1002,9 +1004,9 @@ Definition Bexact_inverse_mantissa := Z.iter (prec - 1) xO xH.
 Remark Bexact_inverse_mantissa_value:
   Zpos Bexact_inverse_mantissa = 2 ^ (prec - 1).
 Proof.
-  assert (REC: forall n, Z.pos (nat_iter n xO xH) = 2 ^ (Z.of_nat n)).
+  assert (REC: forall n, Z.pos (nat_rect _ xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)).
   { induction n. reflexivity.
-    simpl nat_iter. transitivity (2 * Z.pos (nat_iter n xO xH)). reflexivity.
+    simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity.
     rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega.
     change (2 ^ 1) with 2. ring. }
   red in prec_gt_0_.
@@ -1015,12 +1017,12 @@ Qed.
 Remark Bexact_inverse_mantissa_digits2_pos:
   Z.pos (digits2_pos Bexact_inverse_mantissa) = prec.
 Proof.
-  assert (DIGITS: forall n, digits2_pos (nat_iter n xO xH) = Pos.of_nat (n+1)).
+  assert (DIGITS: forall n, digits2_pos (nat_rect _ xH (fun _ => xO) n) = Pos.of_nat (n+1)).
   { induction n; simpl. auto. rewrite IHn. destruct n; auto. }
   red in prec_gt_0_.
   unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS.
   rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega.
-  destruct prec; try  discriminate. rewrite NPeano.Nat.sub_add.
+  destruct prec; try  discriminate. rewrite Nat.sub_add.
   simpl. rewrite Pos2Nat.id. auto.
   simpl. zify; omega.
 Qed.
@@ -1039,7 +1041,7 @@ Qed.
 
 Program Definition Bexact_inverse (f: binary_float) : option binary_float :=
   match f with
-  | B754_finite s m e B =>
+  | B754_finite _ _ s m e B =>
       if positive_eq_dec m Bexact_inverse_mantissa then
       let e' := -e - (prec - 1) * 2 in
       if Z_le_dec emin e' then
@@ -1125,7 +1127,7 @@ Lemma pos_pow_spec:
   forall x y, Z.pos (pos_pow x y) = Z.pos x ^ Z.pos y.
 Proof.
   intros x.
-  assert (REC: forall y a, Pos.iter y (Pos.mul x) a = Pos.mul (pos_pow x y) a).
+  assert (REC: forall y a, Pos.iter (Pos.mul x) a y = Pos.mul (pos_pow x y) a).
   { induction y; simpl; intros.
   - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto.
   - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto.
@@ -1347,10 +1349,10 @@ Let binary_float2 := binary_float prec2 emax2.
 
 Definition Bconv (conv_nan: bool -> nan_pl prec1 -> bool * nan_pl prec2) (md: mode) (f: binary_float1) : binary_float2 :=
   match f with
-    | B754_nan s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl
-    | B754_infinity s => B754_infinity _ _ s
-    | B754_zero s => B754_zero _ _ s
-    | B754_finite s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s
+    | B754_nan _ _ s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl
+    | B754_infinity _ _ s => B754_infinity _ _ s
+    | B754_zero _ _ s => B754_zero _ _ s
+    | B754_finite _ _ s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s
   end.
 
 Theorem Bconv_correct:
diff --git a/lib/Floats.v b/lib/Floats.v
index cf25852e..51b0c415 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -109,7 +109,7 @@ Module Float.
 (** Transform a Nan payload to a quiet Nan payload. *)
 
 Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 :=
-  Pos.lor pl (nat_iter 51 xO xH).
+  Pos.lor pl (iter_nat xO 51 xH).
 Next Obligation.
   destruct pl.
   simpl. rewrite Z.ltb_lt in *.
@@ -147,7 +147,7 @@ Definition expand_pl (pl: nan_pl 24) : nan_pl 53.
 Proof.
   refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _).
   abstract (
-    destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_pos;
+    destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_rect, Fcore_digits.digits2_pos;
     fold (Fcore_digits.digits2_pos x);
     rewrite Z.ltb_lt in *;
     zify; omega).
@@ -163,7 +163,7 @@ Definition reduce_pl (pl: nan_pl 53) : nan_pl 24.
 Proof.
   refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _).
   abstract (
-    destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter;
+    destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_rect;
     rewrite Z.ltb_lt in *;
     assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) =
                       (Fcore_digits.digits2_pos x - 1)%positive)
@@ -473,13 +473,11 @@ Proof.
     apply Rgt_ge; apply Rcompare_Gt_inv; auto.
   }
   assert (EQ: ZofB_range _ _ (sub x y) Int.min_signed Int.max_signed = Some (p - Int.unsigned ox8000_0000)).
-  {
-    apply ZofB_range_minus. exact E.
+  { apply ZofB_range_minus. exact E.
     compute_this (Int.unsigned ox8000_0000). smart_omega.
     apply Rge_le; auto.
   }
-  unfold to_int; rewrite EQ. simpl. f_equal. unfold Int.sub. f_equal. f_equal.
-  symmetry; apply Int.unsigned_repr. omega.
+  unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by omega. auto.
 Qed.
 
 (** Conversions from ints to floats can be defined as bitwise manipulations
@@ -538,7 +536,7 @@ Theorem of_intu_from_words:
 Proof.
   intros. pose proof (Int.unsigned_range x).
   rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus.
-  unfold of_intu. f_equal. rewrite Int.unsigned_zero. omega.
+  unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. omega.
   apply integer_representable_n; auto; smart_omega.
   apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega.
 Qed.
@@ -565,7 +563,7 @@ Proof.
   rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned.
   change (Int.unsigned ox8000_0000) with Int.half_modulus.
   unfold sub. rewrite BofZ_minus.
-  unfold of_int. f_equal. omega.
+  unfold of_int. apply f_equal. omega.
   apply integer_representable_n; auto; smart_omega.
   apply integer_representable_n; auto; smart_omega.
 Qed.
@@ -674,7 +672,7 @@ Proof.
      with ((xh - 2^20) * 2^32)
        by (compute_this p; compute_this Int.half_modulus; ring).
   unfold add. rewrite BofZ_plus.
-  unfold of_long. f_equal.
+  unfold of_long. apply f_equal.
   rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''.
   fold xh; fold xl. compute_this (two_p 32); ring.
   apply integer_representable_n2p; auto.
@@ -831,7 +829,7 @@ Module Float32.
 (** ** NaN payload manipulations *)
 
 Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 :=
-  Pos.lor pl (nat_iter 22 xO xH).
+  Pos.lor pl (iter_nat xO 22 xH).
 Next Obligation.
   destruct pl.
   simpl. rewrite Z.ltb_lt in *.
@@ -1280,4 +1278,3 @@ Global Opaque
   Float32.to_int Float32.to_intu Float32.to_long Float32.to_longu
   Float32.add Float32.sub Float32.mul Float32.div Float32.cmp
   Float32.to_bits Float32.of_bits.
-
diff --git a/lib/Integers.v b/lib/Integers.v
index a0140e57..316dfb52 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -53,7 +53,7 @@ Definition swap_comparison (c: comparison): comparison :=
 (** * Parameterization by the word size, in bits. *)
 
 Module Type WORDSIZE.
-  Variable wordsize: nat.
+  Parameter wordsize: nat.
   Axiom wordsize_not_zero: wordsize <> 0%nat.
 End WORDSIZE.
 
@@ -3378,7 +3378,7 @@ Proof.
     repeat rewrite unsigned_repr. tauto.
     generalize wordsize_max_unsigned; omega.
     generalize wordsize_max_unsigned; omega.
-  intros. unfold one_bits in H.
+  unfold one_bits. intros.
   destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]].
   subst i. apply A. apply Z_one_bits_range with (unsigned x); auto.
 Qed.
@@ -3576,8 +3576,8 @@ Proof.
   intros.
   destruct (andb_prop _ _ H1). clear H1.
   destruct (andb_prop _ _ H2). clear H2.
-  exploit proj_sumbool_true. eexact H1. intro A; clear H1.
-  exploit proj_sumbool_true. eexact H4. intro B; clear H4.
+  apply proj_sumbool_true in H1.
+  apply proj_sumbool_true in H4.
   assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1).
   destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto.
   clear H3.
diff --git a/lib/Intv.v b/lib/Intv.v
index 090ff408..57d946e3 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -248,7 +248,7 @@ Next Obligation.
   destruct H2. congruence. auto.
 Qed.
 Next Obligation.
-  exists wildcard'0; split; auto. omega.
+  exists wildcard'; split; auto. omega.
 Qed.
 Next Obligation.
   exists (hi - 1); split; auto. omega.
@@ -310,7 +310,3 @@ Hint Resolve
   disjoint_range
   in_shift in_shift_inv
   in_elements elements_in : intv.
-
-
-
-
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 352b4479..4455e22f 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -33,21 +33,21 @@ Local Unset Case Analysis Schemes.
 
 Module Type SEMILATTICE.
 
-  Variable t: Type.
-  Variable eq: t -> t -> Prop.
-  Hypothesis eq_refl: forall x, eq x x.
-  Hypothesis eq_sym: forall x y, eq x y -> eq y x.
-  Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
-  Variable beq: t -> t -> bool.
-  Hypothesis beq_correct: forall x y, beq x y = true -> eq x y.
-  Variable ge: t -> t -> Prop.
-  Hypothesis ge_refl: forall x y, eq x y -> ge x y.
-  Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Variable bot: t.
-  Hypothesis ge_bot: forall x, ge x bot.
-  Variable lub: t -> t -> t.
-  Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
-  Hypothesis ge_lub_right: forall x y, ge (lub x y) y.
+  Parameter t: Type.
+  Parameter eq: t -> t -> Prop.
+  Axiom eq_refl: forall x, eq x x.
+  Axiom eq_sym: forall x y, eq x y -> eq y x.
+  Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+  Parameter beq: t -> t -> bool.
+  Axiom beq_correct: forall x y, beq x y = true -> eq x y.
+  Parameter ge: t -> t -> Prop.
+  Axiom ge_refl: forall x y, eq x y -> ge x y.
+  Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Parameter bot: t.
+  Axiom ge_bot: forall x, ge x bot.
+  Parameter lub: t -> t -> t.
+  Axiom ge_lub_left: forall x y, ge (lub x y) x.
+  Axiom ge_lub_right: forall x y, ge (lub x y) y.
 
 End SEMILATTICE.
 
@@ -57,8 +57,8 @@ End SEMILATTICE.
 Module Type SEMILATTICE_WITH_TOP.
 
   Include Type SEMILATTICE.
-  Variable top: t.
-  Hypothesis ge_top: forall x, ge top x.
+  Parameter top: t.
+  Axiom ge_top: forall x, ge top x.
 
 End SEMILATTICE_WITH_TOP.
 
diff --git a/lib/Maps.v b/lib/Maps.v
index 99720b6e..de9a33b8 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -44,24 +44,24 @@ Set Implicit Arguments.
 (** * The abstract signatures of trees *)
 
 Module Type TREE.
-  Variable elt: Type.
-  Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
-  Variable t: Type -> Type.
-  Variable empty: forall (A: Type), t A.
-  Variable get: forall (A: Type), elt -> t A -> option A.
-  Variable set: forall (A: Type), elt -> A -> t A -> t A.
-  Variable remove: forall (A: Type), elt -> t A -> t A.
+  Parameter elt: Type.
+  Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}.
+  Parameter t: Type -> Type.
+  Parameter empty: forall (A: Type), t A.
+  Parameter get: forall (A: Type), elt -> t A -> option A.
+  Parameter set: forall (A: Type), elt -> A -> t A -> t A.
+  Parameter remove: forall (A: Type), elt -> t A -> t A.
 
   (** The ``good variables'' properties for trees, expressing
     commutations between [get], [set] and [remove]. *)
-  Hypothesis gempty:
+  Axiom gempty:
     forall (A: Type) (i: elt), get i (empty A) = None.
-  Hypothesis gss:
+  Axiom gss:
     forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
-  Hypothesis gso:
+  Axiom gso:
     forall (A: Type) (i j: elt) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
-  Hypothesis gsspec:
+  Axiom gsspec:
     forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then Some x else get i m.
   (* We could implement the following, but it's not needed for the moment.
@@ -72,18 +72,18 @@ Module Type TREE.
     forall (A: Type) (i: elt) (m: t A) (v: A),
     get i m = None -> remove i m = m.
   *)
-  Hypothesis grs:
+  Axiom grs:
     forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
-  Hypothesis gro:
+  Axiom gro:
     forall (A: Type) (i j: elt) (m: t A),
     i <> j -> get i (remove j m) = get i m.
-  Hypothesis grspec:
+  Axiom grspec:
     forall (A: Type) (i j: elt) (m: t A),
     get i (remove j m) = if elt_eq i j then None else get i m.
 
   (** Extensional equality between trees. *)
-  Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
-  Hypothesis beq_correct:
+  Parameter beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
+  Axiom beq_correct:
     forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A),
     beq eqA t1 t2 = true <->
     (forall (x: elt),
@@ -94,60 +94,60 @@ Module Type TREE.
     end).
 
   (** Applying a function to all data of a tree. *)
-  Variable map:
+  Parameter map:
     forall (A B: Type), (elt -> A -> B) -> t A -> t B.
-  Hypothesis gmap:
+  Axiom gmap:
     forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
     get i (map f m) = option_map (f i) (get i m).
 
   (** Same as [map], but the function does not receive the [elt] argument. *)
-  Variable map1:
+  Parameter map1:
     forall (A B: Type), (A -> B) -> t A -> t B.
-  Hypothesis gmap1:
+  Axiom gmap1:
     forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
     get i (map1 f m) = option_map f (get i m).
 
   (** Applying a function pairwise to all data of two trees. *)
-  Variable combine:
+  Parameter combine:
     forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C.
-  Hypothesis gcombine:
+  Axiom gcombine:
     forall (A B C: Type) (f: option A -> option B -> option C),
     f None None = None ->
     forall (m1: t A) (m2: t B) (i: elt),
     get i (combine f m1 m2) = f (get i m1) (get i m2).
 
   (** Enumerating the bindings of a tree. *)
-  Variable elements:
+  Parameter elements:
     forall (A: Type), t A -> list (elt * A).
-  Hypothesis elements_correct:
+  Axiom elements_correct:
     forall (A: Type) (m: t A) (i: elt) (v: A),
     get i m = Some v -> In (i, v) (elements m).
-  Hypothesis elements_complete:
+  Axiom elements_complete:
     forall (A: Type) (m: t A) (i: elt) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
-  Hypothesis elements_keys_norepet:
+  Axiom elements_keys_norepet:
     forall (A: Type) (m: t A),
     list_norepet (List.map (@fst elt A) (elements m)).
-  Hypothesis elements_extensional:
+  Axiom elements_extensional:
     forall (A: Type) (m n: t A),
     (forall i, get i m = get i n) ->
     elements m = elements n.
-  Hypothesis elements_remove:
+  Axiom elements_remove:
     forall (A: Type) i v (m: t A),
     get i m = Some v ->
     exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2.
 
   (** Folding a function over all bindings of a tree. *)
-  Variable fold:
+  Parameter fold:
     forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B.
-  Hypothesis fold_spec:
+  Axiom fold_spec:
     forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   (** Same as [fold], but the function does not receive the [elt] argument. *)
-  Variable fold1:
+  Parameter fold1:
     forall (A B: Type), (B -> A -> B) -> t A -> B -> B.
-  Hypothesis fold1_spec:
+  Axiom fold1_spec:
     forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A),
     fold1 f m v =
     List.fold_left (fun a p => f a (snd p)) (elements m) v.
@@ -156,26 +156,26 @@ End TREE.
 (** * The abstract signatures of maps *)
 
 Module Type MAP.
-  Variable elt: Type.
-  Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
-  Variable t: Type -> Type.
-  Variable init: forall (A: Type), A -> t A.
-  Variable get: forall (A: Type), elt -> t A -> A.
-  Variable set: forall (A: Type), elt -> A -> t A -> t A.
-  Hypothesis gi:
+  Parameter elt: Type.
+  Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}.
+  Parameter t: Type -> Type.
+  Parameter init: forall (A: Type), A -> t A.
+  Parameter get: forall (A: Type), elt -> t A -> A.
+  Parameter set: forall (A: Type), elt -> A -> t A -> t A.
+  Axiom gi:
     forall (A: Type) (i: elt) (x: A), get i (init x) = x.
-  Hypothesis gss:
+  Axiom gss:
     forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
-  Hypothesis gso:
+  Axiom gso:
     forall (A: Type) (i j: elt) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
-  Hypothesis gsspec:
+  Axiom gsspec:
     forall (A: Type) (i j: elt) (x: A) (m: t A),
     get i (set j x m) = if elt_eq i j then x else get i m.
-  Hypothesis gsident:
+  Axiom gsident:
     forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
-  Variable map: forall (A B: Type), (A -> B) -> t A -> t B.
-  Hypothesis gmap:
+  Parameter map: forall (A B: Type), (A -> B) -> t A -> t B.
+  Axiom gmap:
     forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
     get i (map f m) = f(get i m).
 End MAP.
@@ -1040,10 +1040,10 @@ End PMap.
 (** * An implementation of maps over any type that injects into type [positive] *)
 
 Module Type INDEXED_TYPE.
-  Variable t: Type.
-  Variable index: t -> positive.
-  Hypothesis index_inj: forall (x y: t), index x = index y -> x = y.
-  Variable eq: forall (x y: t), {x = y} + {x <> y}.
+  Parameter t: Type.
+  Parameter index: t -> positive.
+  Axiom index_inj: forall (x y: t), index x = index y -> x = y.
+  Parameter eq: forall (x y: t), {x = y} + {x <> y}.
 End INDEXED_TYPE.
 
 Module IMap(X: INDEXED_TYPE).
@@ -1148,8 +1148,8 @@ Module NMap := IMap(NIndexed).
 (** * An implementation of maps over any type with decidable equality *)
 
 Module Type EQUALITY_TYPE.
-  Variable t: Type.
-  Variable eq: forall (x y: t), {x = y} + {x <> y}.
+  Parameter t: Type.
+  Parameter eq: forall (x y: t), {x = y} + {x <> y}.
 End EQUALITY_TYPE.
 
 Module EMap(X: EQUALITY_TYPE) <: MAP.
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 76dd6b31..27278b01 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -26,96 +26,96 @@ Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
 
 Module Type MAP.
-  Variable elt: Type.
-  Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}.
-  Variable t: Type -> Type.
-  Variable empty: forall (A: Type), t A.
-  Variable get: forall (A: Type), elt -> t A -> option A.
-  Variable set: forall (A: Type), elt -> A -> t A -> t A.
-  Hypothesis gempty: forall (A: Type) (x: elt), get x (empty A) = None.
-  Hypothesis gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A),
+  Parameter elt: Type.
+  Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}.
+  Parameter t: Type -> Type.
+  Parameter empty: forall (A: Type), t A.
+  Parameter get: forall (A: Type), elt -> t A -> option A.
+  Parameter set: forall (A: Type), elt -> A -> t A -> t A.
+  Axiom gempty: forall (A: Type) (x: elt), get x (empty A) = None.
+  Axiom gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A),
     get x (set y v m) = if elt_eq x y then Some v else get x m.
 End MAP.
 
 Unset Implicit Arguments.
 
 Module Type UNIONFIND.
-  Variable elt: Type.
-  Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}.
-  Variable t: Type.
+  Parameter elt: Type.
+  Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}.
+  Parameter t: Type.
 
-  Variable repr: t -> elt -> elt.
-  Hypothesis repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a.
+  Parameter repr: t -> elt -> elt.
+  Axiom repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a.
 
   Definition sameclass (uf: t) (a b: elt) : Prop := repr uf a = repr uf b.
-  Hypothesis sameclass_refl:
+  Axiom sameclass_refl:
     forall uf a, sameclass uf a a.
-  Hypothesis sameclass_sym:
+  Axiom sameclass_sym:
     forall uf a b, sameclass uf a b -> sameclass uf b a.
-  Hypothesis sameclass_trans:
+  Axiom sameclass_trans:
     forall uf a b c,
     sameclass uf a b -> sameclass uf b c -> sameclass uf a c.
-  Hypothesis sameclass_repr:
+  Axiom sameclass_repr:
     forall uf a, sameclass uf a (repr uf a).
 
-  Variable empty: t.
-  Hypothesis repr_empty:
+  Parameter empty: t.
+  Axiom repr_empty:
     forall a, repr empty a = a.
-  Hypothesis sameclass_empty:
+  Axiom sameclass_empty:
     forall a b, sameclass empty a b -> a = b.
 
-  Variable find: t -> elt -> elt * t.
-  Hypothesis find_repr:
+  Parameter find: t -> elt -> elt * t.
+  Axiom find_repr:
     forall uf a, fst (find uf a) = repr uf a.
-  Hypothesis find_unchanged:
+  Axiom find_unchanged:
     forall uf a x, repr (snd (find uf a)) x = repr uf x.
-  Hypothesis sameclass_find_1:
+  Axiom sameclass_find_1:
     forall uf a x y, sameclass (snd (find uf a)) x y <-> sameclass uf x y.
-  Hypothesis sameclass_find_2:
+  Axiom sameclass_find_2:
     forall uf a, sameclass uf a (fst (find uf a)).
-  Hypothesis sameclass_find_3:
+  Axiom sameclass_find_3:
     forall uf a, sameclass (snd (find uf a)) a (fst (find uf a)).
 
-  Variable union: t -> elt -> elt -> t.
-  Hypothesis repr_union_1:
+  Parameter union: t -> elt -> elt -> t.
+  Axiom repr_union_1:
     forall uf a b x, repr uf x <> repr uf a -> repr (union uf a b) x = repr uf x.
-  Hypothesis repr_union_2:
+  Axiom repr_union_2:
     forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b.
-  Hypothesis repr_union_3:
+  Axiom repr_union_3:
     forall uf a b, repr (union uf a b) b = repr uf b.
-  Hypothesis sameclass_union_1:
+  Axiom sameclass_union_1:
     forall uf a b, sameclass (union uf a b) a b.
-  Hypothesis sameclass_union_2:
+  Axiom sameclass_union_2:
     forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y.
-  Hypothesis sameclass_union_3:
+  Axiom sameclass_union_3:
     forall uf a b x y,
     sameclass (union uf a b) x y ->
        sameclass uf x y
     \/ sameclass uf x a /\ sameclass uf y b
     \/ sameclass uf x b /\ sameclass uf y a.
 
-  Variable merge: t -> elt -> elt -> t.
-  Hypothesis repr_merge:
+  Parameter merge: t -> elt -> elt -> t.
+  Axiom repr_merge:
     forall uf a b x, repr (merge uf a b) x = repr (union uf a b) x.
-  Hypothesis sameclass_merge:
+  Axiom sameclass_merge:
     forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y.
 
-  Variable path_ord: t -> elt -> elt -> Prop.
-  Hypothesis path_ord_wellfounded:
+  Parameter path_ord: t -> elt -> elt -> Prop.
+  Axiom path_ord_wellfounded:
     forall uf, well_founded (path_ord uf).
-  Hypothesis path_ord_canonical:
+  Axiom path_ord_canonical:
     forall uf x y, repr uf x = x -> ~path_ord uf y x.
-  Hypothesis path_ord_merge_1:
+  Axiom path_ord_merge_1:
     forall uf a b x y,
     path_ord uf x y -> path_ord (merge uf a b) x y.
-  Hypothesis path_ord_merge_2:
+  Axiom path_ord_merge_2:
     forall uf a b,
     repr uf a <> repr uf b -> path_ord (merge uf a b) b (repr uf a).
 
-  Variable pathlen: t -> elt -> nat.
-  Hypothesis pathlen_zero:
+  Parameter pathlen: t -> elt -> nat.
+  Axiom pathlen_zero:
     forall uf a, repr uf a = a <-> pathlen uf a = O.
-  Hypothesis pathlen_merge:
+  Axiom pathlen_merge:
     forall uf a b x,
     pathlen (merge uf a b) x =
       if elt_eq (repr uf a) (repr uf b) then
@@ -124,7 +124,7 @@ Module Type UNIONFIND.
         pathlen uf x + pathlen uf b + 1
       else
         pathlen uf x.
-  Hypothesis pathlen_gt_merge:
+  Axiom pathlen_gt_merge:
     forall uf a b x y,
     repr uf x = repr uf y ->
     pathlen uf x > pathlen uf y ->
@@ -652,21 +652,21 @@ Qed.
 Next Obligation.
   (* a <> b*)
   destruct (find_x a')
-  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
+  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous.
   apply repr_some_diff. auto.
 Qed.
 Next Obligation.
-  destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
+  destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous.
   rewrite B. apply repr_some. auto.
 Qed.
 Next Obligation.
   split.
   destruct (find_x a')
-  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
+  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous.
   symmetry. apply repr_some. auto.
   intros. rewrite repr_compress.
   destruct (find_x a')
-  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto.
+  as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. auto.
 Qed.
 Next Obligation.
   split; auto. symmetry. apply repr_none. auto.
diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v
index 4f80822e..a1e4b4ff 100644
--- a/lib/Wfsimpl.v
+++ b/lib/Wfsimpl.v
@@ -18,7 +18,7 @@
   to be defined have non-dependent types, and function extensionality is assumed. *)
 
 Require Import Axioms.
-Require Import Wf.
+Require Import Init.Wf.
 Require Import Wf_nat.
 
 Set Implicit Arguments.
@@ -65,4 +65,3 @@ Qed.
 End FIXM.
 
 
-