Imported Upstream version 8.3upstream/8.3

7 files changed, 30 insertions, 32 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 1aad3cec..2bfebfd8 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -15,7 +15,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
@@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff.
 
 (** Leibniz equality. *)
 
-Program Instance eq_Reflexive : Reflexive (@eq A).
-Program Instance eq_Symmetric : Symmetric (@eq A).
-Program Instance eq_Transitive : Transitive (@eq A).
+Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A.
+Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A.
+Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 7b64ded7..cf0449f8 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -8,7 +8,7 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *)
+(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *)
 
 (** * FMapAVL *)
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index be7becda..c8c5e3d6 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (** * This module proves the validity of
     - well-founded recursion (also known as course of values)
@@ -36,6 +36,8 @@ Section Well_founded.
   destruct 1; trivial.
  Defined.
 
+ Global Implicit Arguments Acc_inv [x y] [x].
+
  (** A relation is well-founded if every element is accessible *)
 
  Definition well_founded := forall a:A, Acc a.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 2764d1b4..53e12723 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 13359 2010-07-30 08:46:55Z herbelin $ i*)
+(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -33,7 +33,8 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 Definition block {A : Type} (a : A) := a.
 
 Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
-Ltac unblock_goal := unfold block in *.
+Ltac unblock_goal := unfold block at 1.
+Ltac unblock_all := unfold block in *.
 
 (** Notation for heterogenous equality. *)
 
@@ -41,8 +42,8 @@ Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
 (** Notation for the single element of [x = x] and [x ~= x]. *)
 
-Implicit Arguments eq_refl [[A] [x]].
-Implicit Arguments JMeq_refl [[A] [x]].
+Implicit Arguments eq_refl [[A] [x]] [A].
+Implicit Arguments JMeq_refl [[A] [x]] [A].
 
 (** Do something on an heterogeneous equality appearing in the context. *)
 
@@ -224,7 +225,7 @@ Ltac simplify_eqs :=
 
 Ltac simplify_IH_hyps := repeat
   match goal with
-    | [ hyp : _ |- _ ] => specialize_eqs hyp
+    | [ hyp : context [ block _ ] |- _ ] => specialize_eqs hyp ; unfold block in hyp
   end.
 
 (** We split substitution tactics in the two directions depending on which 
@@ -389,18 +390,18 @@ Tactic Notation "intro_block_id" ident(H) :=
   (is_introduced H ; block_goal ; revert_until H) ||
     (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
 
-Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_all.
 
 Ltac do_intros H :=
   (try intros until H) ; (intro_block_id H || intro_block H).
 
-Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H.
+Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; block_goal ; tac H ; unblock_goal.
 
 Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim.
 
 Ltac do_depind tac H := 
-  (try intros until H) ; intro_block H ;
-  generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+  do_intros H ; generalize_eqs_vars H ; block_goal ; tac H ; 
+  unblock_goal ; simplify_dep_elim ; simplify_IH_hyps ; unblock_all.
 
 (** To dependent elimination on some hyp. *)
 
@@ -417,8 +418,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depelim' tac H :=
-  (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; 
-    simplify_IH_hyps ; unblock_goal.
+  (try intros until H) ; block_goal ; generalize_eqs H ; block_goal ; tac H ; unblock_goal ;
+    simplify_dep_elim ; simplify_IH_hyps ; unblock_all.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 0e6b2909..2f89ff53 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Syntax.v 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 (** Custom notations and implicits for Coq prelude definitions.
 
@@ -20,16 +20,14 @@ Notation " () " := tt.
 
 (** Set maximally inserted implicit arguments for standard definitions. *)
 
-Implicit Arguments eq [[A]].
-
 Implicit Arguments Some [[A]].
 Implicit Arguments None [[A]].
 
-Implicit Arguments inl [[A] [B]].
-Implicit Arguments inr [[A] [B]].
+Implicit Arguments inl [[A] [B]] [A].
+Implicit Arguments inr [[A] [B]] [B].
 
-Implicit Arguments left [[A] [B]].
-Implicit Arguments right [[A] [B]].
+Implicit Arguments left [[A] [B]] [A].
+Implicit Arguments right [[A] [B]] [B].
 
 Implicit Arguments pair [[A] [B]].
 Implicit Arguments fst [[A] [B]].
@@ -50,8 +48,8 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
 Require Import Bvector.
 
-Implicit Arguments Vnil [[A]].
-Implicit Arguments Vcons [[A] [n]].
+Implicit Arguments Vnil [[A]] [].
+Implicit Arguments Vcons [[A] [n]] [].
 
 (** Treating n-ary exists *)
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 4159f436..4ca49c41 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)
@@ -16,8 +16,6 @@ Require Import ProofIrrelevance.
 
 Open Local Scope program_scope.
 
-Implicit Arguments Acc_inv [A R x y].
-
 Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index d205c0e0..382511d9 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: Equalities.v 12662 2010-01-13 16:53:01Z letouzey $ *)
+(* $Id: Equalities.v 13475 2010-09-29 14:33:13Z letouzey $ *)
 
 Require Export RelationClasses.
 
@@ -176,8 +176,7 @@ Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
 
 Module Type UsualIsEq (E:UsualEq) <: IsEq E.
  (* No Instance syntax to avoid saturating the Equivalence tables *)
- Lemma eq_equiv : Equivalence E.eq.
- Proof. exact eq_equivalence. Qed.
+ Definition eq_equiv : Equivalence E.eq := eq_equivalence.
 End UsualIsEq.
 
 Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.