9 files changed, 15 insertions, 12 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index f4017024..a298032f 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: Basics.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** Standard functions and combinators.
 
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 39fb4093..e61c7027 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: Combinators.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** * Proofs about standard combinators, exports functional extensionality.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 1e139497..2764d1b4 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$ i*)
+(*i $Id: Equality.v 13359 2010-07-30 08:46:55Z herbelin $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -15,6 +15,9 @@ Require Export JMeq.
 
 Require Import Coq.Program.Tactics.
 
+Local Notation "'Π'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
 Ltac is_ground_goal := 
   match goal with
     |- ?T => is_ground T
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 71be3478..929fc47c 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: Program.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index ce5f1068..9d82fde8 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: Subset.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** Tactics related to subsets and proof irrelevance. *)
 
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 05bf2ea6..0e6b2909 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$ *)
+(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** Custom notations and implicits for Coq prelude definitions.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 91a8edff..333dd7a6 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$ i*)
+(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
@@ -101,7 +101,7 @@ Ltac revert_last :=
     [ H : _ |- _ ] => revert H
   end.
 
-(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *)
+(** Repeatedly reverse the last hypothesis, putting everything in the goal. *)
 
 Ltac reverse := repeat revert_last.
 
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index f2aad800..b2b5d4be 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Utils.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** Various syntaxic shortands that are useful with [Program]. *)
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d16e900f..4159f436 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$ *)
+(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)
@@ -214,7 +214,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ ?arg ] =>
+        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end
@@ -251,6 +251,6 @@ Module WfExtensionality.
 
   Ltac unfold_sub f fargs :=
     set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
-      rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
+      rewrite fix_sub_eq_ext ; repeat fold_sub f ; simpl proj1_sig.
 
 End WfExtensionality.