Imported Upstream version 8.3pl1upstream/8.3pl1

6 files changed, 49 insertions, 37 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 8f6c59fd..052d9c92 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: NMake_gen.ml 13734 2010-12-21 18:21:56Z letouzey $ i*)
 
 (*S NMake_gen.ml : this file generates NMake.v *)
 
@@ -1299,7 +1299,7 @@ let _ =
   pr "   (iter _";
   for i = 0 to size do
     pr "      compare_%i" i;
-    pr "      (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
+    pr "      (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
     pr "      (fun n => comparen_%i (S n))" i;
   done;
   pr "      comparenm).";
@@ -1339,9 +1339,9 @@ let _ =
 
   pp " Let spec_opp_compare: forall c (u v: Z),";
   pp "  match c with Eq => u = v | Lt => u < v | Gt => u > v end ->";
-  pp "  match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end.";
+  pp "  match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end.";
   pp " Proof.";
-  pp " intros c u v; case c; unfold opp_compare; auto with zarith.";
+  pp " intros c u v; case c; unfold CompOpp; auto with zarith.";
   pp " Qed.";
   pp "";
 
@@ -1362,7 +1362,7 @@ let _ =
   pp "                      end)";
   for i = 0 to size do
     pp "      compare_%i" i;
-    pp "      (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
+    pp "      (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
     pp "      (fun n => comparen_%i (S n)) _ _ _" i;
   done;
   pp "      comparenm _).";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index a531b92e..3741c95d 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i*)
 
 Require Import ZArith.
 Require Import BigNumPrelude.
@@ -260,13 +260,6 @@ Section ReduceRec.
 
 End ReduceRec.
 
-Definition opp_compare cmp :=
-  match cmp with
-  | Lt => Gt
-  | Eq => Eq
-  | Gt => Lt
-  end.
-
 Section CompareRec.
 
  Variable wm w : Type.
@@ -447,7 +440,7 @@ End AddS.
   | Lt => y < x
   | Gt => y > x
   end ->
-  match opp_compare u with
+  match CompOpp u with
   | Eq => x = y
   | Lt => x < y
   | Gt => x > y
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 53e12723..b9eb8f80 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -320,19 +320,35 @@ Hint Unfold solution_left solution_right deletion simplification_heq
    constructor forms). Compare with the lemma 16 of the paper.
    We don't have a [noCycle] procedure yet. *)
 
+Ltac block_equality id :=
+  match type of id with
+    | @eq ?A ?t ?u => change (block (@eq A t u)) in id
+    | _ => idtac
+  end.
+
+Ltac revert_blocking_until id := 
+  Tactics.on_last_hyp ltac:(fun id' =>
+    match id' with
+      | id => idtac
+      | _ => block_equality id' ; revert id' ; revert_blocking_until id
+    end).
+
 Ltac simplify_one_dep_elim_term c :=
   match c with
     | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
-    | eq (existT _ _ _) (existT _ _ _) -> _ =>
+    | eq (existT _ ?p _) (existT _ ?q _) -> _ =>
       refine (simplification_existT2 _ _ _ _ _ _ _) ||
-        refine (simplification_existT1 _ _ _ _ _ _ _ _)
+        match goal with
+          | H : p = q |- _ => intro
+          | _ => refine (simplification_existT1 _ _ _ _ _ _ _ _)
+        end
     | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
-        move hyp before x ; revert_until hyp ; generalize dependent x ;
+        move hyp before x ; revert_blocking_until hyp ; generalize dependent x ;
           refine (solution_left _ _ _ _)(*  ; intros until 0 *)) ||
       (let hyp := fresh in intros hyp ;
-        move hyp before y ; revert_until hyp ; generalize dependent y ;
+        move hyp before y ; revert_blocking_until hyp ; generalize dependent y ;
           refine (solution_right _ _ _ _)(*  ; intros until 0 *))
     | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 333dd7a6..4a41d9c9 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*)
 
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
@@ -308,11 +308,14 @@ Ltac program_simplify :=
   subst*; autoinjections ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).
 
-Ltac program_solve_wf :=
+(** We only try to solve proposition goals automatically. *)
+
+Ltac program_solve :=
   match goal with
-    |- well_founded _ => auto with *
+    | |- well_founded _ => auto with *
+    | |- ?T => match type of T with Prop => auto end
   end.
 
-Ltac program_simpl := program_simplify ; auto; try program_solve_wf.
+Ltac program_simpl := program_simplify ; try program_solve.
 
 Obligation Tactic := program_simpl.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index e576db2b..04de1bfc 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Mergesort.v 13678 2010-12-04 10:34:28Z herbelin $ i*)
 
 (** A modular implementation of mergesort (the complexity is O(n.log n) in
    the length of the list) *)
@@ -61,6 +61,7 @@ Fixpoint merge l1 l2 :=
 
     For instance, here is how [6;2;3;1;5] is sorted:
 
+<<
        operation             stack                list
        iter_merge            []                   [6;2;3;1;5]
     =  append_list_to_stack  [ + [6]]             [2;3;1;5]
@@ -77,7 +78,7 @@ Fixpoint merge l1 l2 :=
     =  append_list_to_stack  [[1;2;3;6];; + [5]]  []
     -> merge_stack           [[1;2;3;6];;[5]]
     =                                             [1;2;3;5;6]
-
+>>
     The complexity of the algorithm is n*log n, since there are
     2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0
     of length 2^p for a list of length 2^p. The algorithm does not need
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 2a615311..357d0b7e 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: BinInt.v 13697 2010-12-09 18:48:04Z herbelin $ i*)
 
 (***********************************************************)
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
@@ -223,7 +223,6 @@ Qed.
 
 
 (**********************************************************************)
-
 (** ** Properties of opposite on binary integer numbers *)
 
 Theorem Zopp_0 : Zopp Z0 = Z0.
@@ -270,21 +269,21 @@ Qed.
 (**********************************************************************)
 (** * Properties of the addition on integers *)
 
-(** ** zero is left neutral for addition *)
+(** ** Zero is left neutral for addition *)
 
 Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
 Proof.
   intro x; destruct x; reflexivity.
 Qed.
 
-(** *** zero is right neutral for addition *)
+(** ** Zero is right neutral for addition *)
 
 Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
 Proof.
   intro x; destruct x; reflexivity.
 Qed.
 
-(** ** addition is commutative *)
+(** ** Addition is commutative *)
 
 Theorem Zplus_comm : forall n m:Z, n + m = m + n.
 Proof.
@@ -296,7 +295,7 @@ Proof.
   rewrite Pplus_comm; reflexivity.
 Qed.
 
-(** ** opposite distributes over addition *)
+(** ** Opposite distributes over addition *)
 
 Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 Proof.
@@ -310,7 +309,7 @@ Proof.
 intro; unfold Zsucc; now rewrite Zopp_plus_distr.
 Qed.
 
-(** ** opposite is inverse for addition *)
+(** ** Opposite is inverse for addition *)
 
 Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
 Proof.
@@ -327,7 +326,7 @@ Qed.
 
 Hint Local Resolve Zplus_0_l Zplus_0_r.
 
-(** ** addition is associative *)
+(** ** Addition is associative *)
 
 Lemma weak_assoc :
   forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
@@ -495,7 +494,7 @@ Proof.
     rewrite (Zplus_comm p n); trivial with arith.
 Qed.
 
-(** ** addition simplifies *)
+(** ** Addition simplifies *)
 
 Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
   intros n m p H; cut (- n + (n + m) = - n + (n + p));
@@ -504,7 +503,7 @@ Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
       | rewrite H; trivial with arith ].
 Qed.
 
-(** ** addition and successor permutes *)
+(** ** Addition and successor permutes *)
 
 Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
 Proof.
@@ -575,7 +574,7 @@ Proof.
     trivial with arith.
 Qed.
 
-(** successor and predecessor are inverse functions *)
+(** ** Successor and predecessor are inverse functions *)
 
 Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
 Proof.
@@ -600,7 +599,7 @@ Proof.
 Qed.
 
 (*************************************************************************)
-(** **  Properties of the direct definition of successor and predecessor *)
+(** ** Properties of the direct definition of successor and predecessor  *)
 
 Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
 Proof.