From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 theories/Program/Equality.v | 10 +++++++---
 theories/Program/Wf.v       | 12 ++++++------
 2 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 99d54755..9681d543 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
+(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*)
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
@@ -479,8 +479,12 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
-Ltac do_ind p := induction p || elim_ind p.
+Ltac introduce p := 
+  first [ match p with _ => idtac end (* Already there *)
+    | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
 Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 12bdf3a7..2083e530 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 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)
@@ -165,7 +165,7 @@ Section Measure_well_founded.
 
   (* Measure relations are well-founded if the underlying relation is well-founded. *)
 
-  Variables T M: Set.
+  Variables T M: Type.
   Variable R: M -> M -> Prop.
   Hypothesis wf: well_founded R.
   Variable m: T -> M.
@@ -191,7 +191,7 @@ End Measure_well_founded.
 
 Section Fix_measure_rects.
 
-  Variable A: Set.
+  Variable A: Type.
   Variable m: A -> nat.
   Variable P: A -> Type.
   Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
@@ -287,7 +287,7 @@ Section Fix_measure_rects.
 
 End Fix_measure_rects.
 
-(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
+(** Tactic to fold a definition based on [Fix_measure_sub]. *)
 
 Ltac fold_sub f :=
   match goal with
@@ -312,8 +312,8 @@ Module WfExtensionality.
   (** For a function defined with Program using a well-founded order. *)
 
   Program Lemma fix_sub_eq_ext :
-    forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
-      (P : A -> Set)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
       (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-- 
cgit v1.2.3