Imported Upstream version 8.5~beta3+dfsg

27 files changed, 156 insertions, 238 deletions

diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
deleted file mode 100755
index 655de34c..00000000
--- a/theories/Arith/intro.tex
+++ /dev/null
@@ -1,55 +0,0 @@
-\section{Arith}\label{Arith}
-
-The {\tt Arith} library deals with various arithmetical notions and 
-their properties.
-
-\subsection*{Standard {\tt Arith} library}
-
-The following files are automatically loaded by {\tt Require Arith}.
-
-\begin{itemize}
-
-\item {\tt Le.v} states and proves properties of the large order {\tt le}.
-
-\item {\tt Lt.v} states and proves properties of the strict order {\tt 
-lt} (especially, the relationship with {\tt le}).
-
-\item {\tt Plus.v} states and proves properties on the addition.
-
-\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}.
-
-\item {\tt Minus.v} defines the difference on 
-{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is 
-{\tt O} if {\tt n} $<$ {\tt p}.
-
-\item {\tt Mult.v} states and proves properties on the multiplication.
-
-\item {\tt Between.v} defines modalities on {\tt nat} and proves properties 
-of them.
-
-\end{itemize}
-
-\subsection*{Additional {\tt Arith} library}
-
-\begin{itemize}
-
-\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state
-and prove various decidability results on {\tt nat}.
-
-\item {\tt Wf\_nat.v} states and proves various induction and recursion 
-principles on {\tt nat}. Especially, recursion for objects measurable by 
-a natural number and recursion on {\tt nat * nat} are provided.
-
-\item {\tt Min.v} defines the minimum of two natural numbers and proves 
-properties of it. 
-
-\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
-the equivalence with Leibniz' equality.
-
-\item {\tt Euclid.v} proves that the euclidean
-division specification is realisable. Conversely, {\tt Div.v} exhibits
-two different algorithms and semi-automatically reconstruct the proof of
-their correctness. These files emphasize the extraction of program vs
-reconstruction of proofs paradigm.
-
-\end{itemize}
diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex
deleted file mode 100644
index 22ee38aa..00000000
--- a/theories/Bool/intro.tex
+++ /dev/null
@@ -1,16 +0,0 @@
-\section{Bool}\label{Bool}
-
-The BOOL library includes the following files:
-
-\begin{itemize}
-
-\item {\tt Bool.v} defines standard operations on booleans and states
-  and proves simple facts on them.
-\item {\tt IfProp.v} defines a disjunction which contains its proof
-  and states its properties.
-\item {\tt Zerob.v} defines the test against 0 on natural numbers and
-  states and proves properties of it.
-\item {\tt Orb.v} states and proves facts on the boolean or.
-\item {\tt DecBool.v} defines a conditional from a proof of
-  decidability and states its properties.
-\end{itemize}
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 048faa91..fdedbf67 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -266,11 +266,12 @@ Section GenericInstances.
     transitivity (y x0)...
   Qed.
 
-  (** The complement of a crelation conserves its proper elements. *)
+  Unset Strict Universe Declaration.
   
-  Program Definition complement_proper
+  (** The complement of a crelation conserves its proper elements. *)
+  Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
           `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-    Proper (RA ==> RA ==> iff) (complement R) := _.
+    Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
   
   Next Obligation.
   Proof.
@@ -280,7 +281,6 @@ Section GenericInstances.
   Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
-
   Program Definition flip_proper
           `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
     Proper (RB ==> RA ==> RC) (flip f) := _.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 1a40e5d5..15cb02d3 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -89,6 +89,11 @@ Section Defs.
   Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
     { }. 
 
+  (** An Equivalence is a PreOrder plus symmetry. *)
+
+  Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 :=
+    { }.
+
   (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
   
   Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
new file mode 100644
index 00000000..b04d5168
--- /dev/null
+++ b/theories/Compat/Coq84.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.4 *)
+(** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
+(** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
+Require Coq.omega.Omega.
+Ltac omega := Coq.omega.Omega.omega.
+
+(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
+Global Set Asymmetric Patterns.
+
+(** See bug 3545 *)
+Global Set Universal Lemma Under Conjunction.
+
+(** In 8.4, [admit] created a new axiom; in 8.5, it just shelves the goal. *)
+Axiom proof_admitted : False.
+Ltac admit := clear; abstract case proof_admitted.
+
+(** In 8.5, [refine] leaves over dependent subgoals. *)
+Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable.
+
+(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
+Ltac constructor_84 := constructor.
+Ltac constructor_84_n n := constructor n.
+Ltac constructor_84_tac tac := once (constructor; tac).
+
+Tactic Notation "constructor" := constructor_84.
+Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
+Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
+
+(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
+Tactic Notation "reflexivity" := reflexivity.
+Tactic Notation "assumption" := assumption.
+Tactic Notation "etransitivity" := etransitivity.
+Tactic Notation "cut" constr(c) := cut c.
+Tactic Notation "exact_no_check" constr(c) := exact_no_check c.
+Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c.
+Tactic Notation "casetype" constr(c) := casetype c.
+Tactic Notation "elimtype" constr(c) := elimtype c.
+Tactic Notation "lapply" constr(c) := lapply c.
+Tactic Notation "transitivity" constr(c) := transitivity c.
+Tactic Notation "left" := left.
+Tactic Notation "eleft" := eleft.
+Tactic Notation "right" := right.
+Tactic Notation "eright" := eright.
+Tactic Notation "constructor" := constructor.
+Tactic Notation "econstructor" := econstructor.
+Tactic Notation "symmetry" := symmetry.
+Tactic Notation "split" := split.
+Tactic Notation "esplit" := esplit.
+
+Global Set Regular Subst Tactic.
+
+(** Some names have changed in the standard library, so we add aliases. *)
+Require Coq.ZArith.Int.
+Module Export Coq.
+  Module Export ZArith.
+    Module Int.
+      Module Z_as_Int.
+        Include Coq.ZArith.Int.Z_as_Int.
+        (* FIXME: Should these get a (compat "8.4")?  Or be moved to Z_as_Int, probably? *)
+        Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing).
+        Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing).
+        Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing).
+      End Z_as_Int.
+    End Int.
+  End ZArith.
+End Coq.
+
+(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
+Require Coq.Numbers.Natural.Peano.NPeano.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
new file mode 100644
index 00000000..1622f2ae
--- /dev/null
+++ b/theories/Compat/Coq85.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.5 *)
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
new file mode 100644
index 00000000..c0c40ab1
--- /dev/null
+++ b/theories/Compat/vo.itarget
@@ -0,0 +1,2 @@
+Coq84.vo
+Coq85.vo
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index ea07a849..fe18686e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -45,8 +45,8 @@ Section Lists.
 
   Definition hd_error (l:list A) :=
     match l with
-      | [] => error
-      | x :: _ => value x
+      | [] => None
+      | x :: _ => Some x
     end.
 
   Definition tl (l:list A) :=
@@ -69,7 +69,7 @@ Section Facts.
   Variable A : Type.
 
 
-  (** *** Genereric facts *)
+  (** *** Generic facts *)
 
   (** Discrimination *)
   Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.
@@ -393,11 +393,11 @@ Section Elts.
     simpl; auto.
   Qed.
 
-  Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
+  Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A :=
     match n, l with
-      | O, x :: _ => value x
+      | O, x :: _ => Some x
       | S n, _ :: l => nth_error l n
-      | _, _ => error
+      | _, _ => None
     end.
 
   Definition nth_default (default:A) (l:list A) (n:nat) : A :=
@@ -622,9 +622,9 @@ Section Elts.
   Qed.
 
 
-  (****************************************)
-  (** ** Counting occurences of a element *)
-  (****************************************)
+  (******************************************)
+  (** ** Counting occurrences of an element *)
+  (******************************************)
 
   Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
@@ -2202,7 +2202,7 @@ Section ForallPairs.
   Proof.
     induction 1.
     inversion 1.
-    simpl; destruct 1; destruct 1; repeat subst; auto.
+    simpl; destruct 1; destruct 1; subst; auto.
     right; left. apply -> Forall_forall; eauto.
     right; right. apply -> Forall_forall; eauto.
   Qed.
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
deleted file mode 100755
index d372de8e..00000000
--- a/theories/Lists/intro.tex
+++ /dev/null
@@ -1,20 +0,0 @@
-\section{Lists}\label{Lists}
-
-This library includes the following files:
-
-\begin{itemize}
-
-\item {\tt List.v} contains definitions of (polymorphic) lists, 
-  functions on lists such as head, tail, map, append and prove some
-  properties of these functions. Implicit arguments are used in this
-  library, so you should read the Reference Manual about implicit
-  arguments before using it.
-
-\item {\tt ListSet.v} contains definitions and properties of finite
-  sets, implemented as lists.
-
-\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
-  co-inductive type. Basic facts are stated and proved. The streams are
-  also polymorphic.
-
-\end{itemize}
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
index 49cc12b8..2f84ebe5 100644
--- a/theories/Logic/WeakFan.v
+++ b/theories/Logic/WeakFan.v
@@ -89,17 +89,14 @@ Qed.
 Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
 Proof.
 intros P Hbar.
-destruct (Hbar (X P)) as (l,(Hd,HP)).
+destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)).
 assert (inductively_barred P l) by (apply (now P l), HP).
 clear Hbar HP.
-induction l.
+induction l as [|a l].
 - assumption.
 - destruct Hd as (Hd,HX).
   apply (IHl Hd). clear IHl.
   destruct a; unfold X in HX; simpl in HX.
-  + apply propagate.
-    * apply H.
-    * destruct HX as (l',(Hl,(HY,Ht))); firstorder.
-      apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial.
-  + destruct HX. exists l. split; auto using Y_approx.
+  + apply propagate; assumption.
+  + exfalso; destruct (HX H).
 Qed.
diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex
deleted file mode 100755
index 1fb294f2..00000000
--- a/theories/Logic/intro.tex
+++ /dev/null
@@ -1,8 +0,0 @@
-\section{Logic}\label{Logic}
-
-This library deals with classical logic and its properties.
-The main file is {\tt Classical.v}.
-
-This library also provides some facts on equalities for dependent
-types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.
-
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
deleted file mode 100644
index bf39bc36..00000000
--- a/theories/NArith/intro.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-\section{Binary natural numbers : NArith}\label{NArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 4e28b5b9..f5e936cf 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -19,7 +19,7 @@ Require Export DoubleType.
   arithmetic. In fact it is more general than that. The only reason
   for this use of 31 is the underlying mecanism for hardware-efficient
   computations by A. Spiwack. Apart from this, a switch to, say,
-  63-bit integers is now just a matter of replacing every occurences
+  63-bit integers is now just a matter of replacing every occurrences
   of 31 by 63. This is actually made possible by the use of
   dependently-typed n-ary constructions for the inductive type
   [int31], its constructor [I31] and any pattern matching on it.
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 6fdf0a2a..376620dd 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -15,7 +15,7 @@ Require Import List.
 (** * Generic dependently-typed operators about [n]-ary functions *)
 
 (** The type of [n]-ary function: [nfun A n B] is
-    [A -> ... -> A -> B] with [n] occurences of [A] in this type. *)
+    [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *)
 
 Fixpoint nfun A n B :=
  match n with
diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex
deleted file mode 100644
index ffce881e..00000000
--- a/theories/PArith/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Binary positive integers : PArith}\label{PArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 67e9a20c..892305b4 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -32,10 +32,3 @@ Require List.
 Export List.ListNotations.
 
 Require Import Bvector.
-
-(** Treating n-ary exists *)
-
-Tactic Notation "exists" constr(x) := exists x.
-Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 0cf8d733..c1d958b9 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -41,7 +41,7 @@ Ltac do_nat n tac :=
 (** Do something on the last hypothesis, or fail *)
 
 Ltac on_last_hyp tac :=
-  match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
+  lazymatch goal with [ H : _ |- _ ] => tac H end.
 
 (** Destructs one pair, without care regarding naming. *)
 
diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex
deleted file mode 100644
index 43317258..00000000
--- a/theories/Reals/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Reals}\label{Reals}
-
-This library contains an axiomatization of real numbers.
-The main file is \texttt{Reals.v}.
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
deleted file mode 100755
index 5056f36f..00000000
--- a/theories/Relations/intro.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{Relations}\label{Relations}
-
-This library develops closure properties of relations.
-
-\begin{itemize}
-\item {\tt Relation\_Definitions.v} deals with the general notions
-  about binary relations (orders, equivalences, ...)
-
-\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
-  closures of relations (by symmetry, by transitivity, ...) and
-  lexicographic orderings.
-
-\item {\tt Operators\_Properties.v} states and proves facts on the
-  various closures of a relation.
-
-\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
-    Relation\_Operators.v} and \\
-    {\tt Operators\_Properties.v} together.
-
-\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
-  confluent relations.
-
-\end{itemize}
diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex
deleted file mode 100644
index 50cd025d..00000000
--- a/theories/Setoids/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Setoids}\label{Setoids}
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
deleted file mode 100755
index 83c2177f..00000000
--- a/theories/Sets/intro.tex
+++ /dev/null
@@ -1,24 +0,0 @@
-\section{Sets}\label{Sets}
-
-This is a library on sets defined by their characteristic predicate.
-It contains the following modules:
-
-\begin{itemize}
-\item {\tt Ensembles.v}
-\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
-\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, 
- {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v},  \\
- {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
-\item {\tt Partial\_Order.v}, {\tt Cpo.v}
-\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, 
- {\tt Powerset\_Classical\_facts.v}
-\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
-\item {\tt Image.v}
-\item {\tt Infinite\_sets.v}
-\item {\tt Integers.v}
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex
deleted file mode 100644
index 64ae4c88..00000000
--- a/theories/Sorting/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Sorting}\label{Sorting}
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b9bf6c7f..2955184f 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -152,18 +152,18 @@ Fixpoint L {m} n (p : t m) : t (m + n) :=
 Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
 Proof.
 induction p.
-  reflexivity.
-  simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
+- reflexivity.
+- simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
 Qed.
-
+ 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (n + m)]
 Really really ineficient !!! *)
 Definition L_R {m} n (p : t m) : t (n + m).
 Proof.
 induction n.
-  exact p.
-  exact ((fix LS k (p: t k) :=
+- exact p.
+- exact ((fix LS k (p: t k) :=
     match p with
       |@F1 k' => @F1 (S k')
       |FS p' => FS (LS _ p')
@@ -178,8 +178,8 @@ Fixpoint R {m} n (p : t m) : t (n + m) :=
 Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).
 Proof.
 induction n.
-  reflexivity.
-  simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
+- reflexivity.
+- simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
 Qed.
 
 Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
@@ -192,9 +192,9 @@ Lemma depair_sanity {m n} (o : t m) (p : t n) :
   proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
 Proof.
 induction o ; simpl.
-  rewrite L_sanity. now rewrite Mult.mult_0_r.
+- rewrite L_sanity. now rewrite Mult.mult_0_r.
 
-  rewrite R_sanity. rewrite IHo.
+- rewrite R_sanity. rewrite IHo.
   rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
     now rewrite (Plus.plus_comm n).
 Qed.
@@ -210,10 +210,10 @@ end.
 Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
 Proof.
 intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal.
-+ now apply EqNat.beq_nat_true.
-+ easy.
-+ easy.
-+ eapply IHp. eassumption.
+- now apply EqNat.beq_nat_true.
+- easy.
+- easy.
+- eapply IHp. eassumption.
 Qed.
 
 Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.
@@ -231,9 +231,9 @@ Qed.
 
 Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}.
 Proof.
- case_eq (eqb x y); intros.
-  + left; now apply eqb_eq.
-  + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+case_eq (eqb x y); intros.
+- left; now apply eqb_eq.
+- right. intros Heq. apply <- eqb_eq in Heq. congruence.
 Defined.
 
 Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 7f4228dd..c5278b91 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -22,6 +22,11 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
    with | eq_refl => conj eq_refl eq_refl
    end.
 
+Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
+Proof.
+intros; apply caseS with (v:=v); intros; reflexivity.
+Defined.
+
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
 is true for the one that use [lt] *)
 
@@ -29,12 +34,12 @@ Lemma eq_nth_iff A n (v1 v2: t A n):
   (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
 Proof.
 split.
-  revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
-    reflexivity.
-    f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
+- revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
+  + reflexivity.
+  + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
     apply H. intros p1 p2 H1;
     apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
-  intros; now f_equal.
+- intros; now f_equal.
 Qed.
 
 Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
@@ -47,8 +52,8 @@ Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
   nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
 Proof.
 subst k2; induction k1.
-  generalize dependent n. apply caseS ; intros. now simpl.
-  generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
+- generalize dependent n. apply caseS ; intros. now simpl.
+- generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
 Qed.
 
 Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
@@ -60,8 +65,8 @@ Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
   nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
 Proof.
 refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
-  revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
-  revert p H.
+- revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
+- revert p H.
   refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
     |S (S n) => fun v => forall p : Fin.t (S n),
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
@@ -84,8 +89,8 @@ Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
   (map f v) [@ p1] = f (v [@ p2]).
 Proof.
 subst p2; induction p1.
-  revert n v; refine (@caseS _ _ _); now simpl.
-  revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
+- revert n v; refine (@caseS _ _ _); now simpl.
+- revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
 
 Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
@@ -93,8 +98,8 @@ Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
 Proof.
 intros; subst p2; subst p3; revert n v w p1.
 refine (@rect2 _ _ _ _ _); simpl.
-  exact (Fin.case0 _).
-  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
+- exact (Fin.case0 _).
+- intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
     now simpl.
 Qed.
 
@@ -103,17 +108,17 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A}
   {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
 Proof.
 assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
-  induction v0.
-    now simpl.
-    intros; simpl. rewrite<- IHv0, assoc. now f_equal.
-  induction v.
-    reflexivity.
-    simpl. intros; now rewrite<- (IHv).
+- induction v0.
+  + now simpl.
+  + intros; simpl. rewrite<- IHv0, assoc. now f_equal.
+- induction v.
+  + reflexivity.
+  + simpl. intros; now rewrite<- (IHv).
 Qed.
 
 Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l.
 Proof.
 induction l.
-  reflexivity.
-  unfold to_list; simpl. now f_equal.
+- reflexivity.
+- unfold to_list; simpl. now f_equal.
 Qed.
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
deleted file mode 100755
index 126071e2..00000000
--- a/theories/Wellfounded/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Well-founded relations}\label{Wellfounded}
-
-This library gives definitions and results about well-founded relations.
-
diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex
deleted file mode 100755
index 21e52c19..00000000
--- a/theories/ZArith/intro.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-\section{Binary integers : ZArith}
-The {\tt ZArith} library deals with binary integers (those used
-by the {\tt Omega} decision tactic).
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 4519070e..b7de4164 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -1,6 +1,7 @@
 Arith/vo.otarget
 Bool/vo.otarget
 Classes/vo.otarget
+Compat/vo.otarget
 FSets/vo.otarget
 MSets/vo.otarget
 MMaps/vo.otarget