Imported Upstream version 8.0pl2upstream/8.0pl2

8 files changed, 39 insertions, 34 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index d44efb56..114a60ee 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith.v,v 1.11.2.1 2004/07/16 19:30:59 herbelin Exp $ i*)
+(*i $Id: Arith.v,v 1.11.2.2 2004/08/03 17:42:42 herbelin Exp $ i*)
 
 Require Export Le.
 Require Export Lt.
@@ -15,7 +15,6 @@ Require Export Gt.
 Require Export Minus.
 Require Export Mult.
 Require Export Between.
-Require Export Minus.
 Require Export Peano_dec.
 Require Export Compare_dec.
-Require Export Factorial.
\ No newline at end of file
+Require Export Factorial.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 2e7cb1fc..e0a18747 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Notations.v,v 1.24.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)
 
-(** These are the notations whose level and associativity is imposed by Coq *)
+(** These are the notations whose level and associativity are imposed by Coq *)
 
-(** Notations for logical connectives *)
+(** Notations for propositional connectives *)
 
 Reserved Notation "x <-> y" (at level 95, no associativity).
 Reserved Notation "x /\ y" (at level 80, right associativity).
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 7e950c17..0fe8a87d 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Berardi.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
 
 (** This file formalizes Berardi's paradox which says that in
    the calculus of constructions, excluded middle (EM) and axiom of
-   choice (AC) implie proof irrelevenace (PI).
+   choice (AC) imply proof irrelevance (PI).
    Here, the axiom of choice is not necessary because of the use
    of inductive types.
 <<
@@ -156,4 +156,4 @@ intros not_true is_true.
 elim not_true; trivial.
 Qed.
 
-End Berardis_paradox.
\ No newline at end of file
+End Berardis_paradox.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index a1f4417c..87d8a70e 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v,v 1.7.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
 
-(* We show that the functional formulation of the axiom of Choice
+(** We show that the functional formulation of the axiom of Choice
    (usual formulation in type theory) is equivalent to its relational
    formulation (only formulation of set theory) + the axiom of
    (parametric) definite description (aka axiom of unique choice) *)
 
-(* This shows that the axiom of choice can be assumed (under its
+(** This shows that the axiom of choice can be assumed (under its
    relational formulation) without known inconsistency with classical logic,
    though definite description conflicts with classical logic *)
 
@@ -80,7 +80,7 @@ intro H; split;
 intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
-(* We show that the guarded relational formulation of the axiom of Choice
+(** We show that the guarded relational formulation of the axiom of Choice
    comes from the non guarded formulation in presence either of the
    independance of premises or proof-irrelevance *)
 
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 55eed096..2b982963 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Diaconescu.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*)
 
-(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
+(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
    entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
    adapted the proof to show that the axiom of choice in equivalence
    classes entails Excluded-Middle in Type Theory.
@@ -27,12 +27,12 @@
 
 Section PredExt_GuardRelChoice_imp_EM.
 
-(* The axiom of extensionality for predicates *)
+(** The axiom of extensionality for predicates *)
 
 Definition PredicateExtensionality :=
   forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
 
-(* From predicate extensionality we get propositional extensionality
+(** From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
 Require Import ClassicalFacts.
@@ -54,7 +54,7 @@ Proof.
   apply (ext_prop_dep_proof_irrel_cic prop_ext).
 Qed.
 
-(* From proof-irrelevance and relational choice, we get guarded
+(** From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
 Require Import ChoiceFacts.
@@ -73,8 +73,8 @@ Proof.
    (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
 Qed.
 
-(* The form of choice we need: there is a functional relation which chooses
-   an element in any non empty subset of bool *)
+(** The form of choice we need: there is a functional relation which chooses
+    an element in any non empty subset of bool *)
 
 Require Import Bool.
 
@@ -90,30 +90,30 @@ Proof.
   exact (fun _ H => H).
 Qed.
 
-(* The proof of the excluded middle *)
-(* Remark: P could have been in Set or Type *)
+(** The proof of the excluded middle *)
+(** Remark: P could have been in Set or Type *)
 
 Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
 intro P.
 
-(* first we exhibit the choice functional relation R *)
+(** first we exhibit the choice functional relation R *)
 destruct AC as [R H].
 
 set (class_of_true := fun b => b = true \/ P).
 set (class_of_false := fun b => b = false \/ P).
 
-(* the actual "decision": is (R class_of_true) = true or false? *)
+(** the actual "decision": is (R class_of_true) = true or false? *)
 destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
 exists true; left; reflexivity.
 destruct H0.
 
-(* the actual "decision": is (R class_of_false) = true or false? *)
+(** the actual "decision": is (R class_of_false) = true or false? *)
 destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
 exists false; left; reflexivity.
 destruct H1.
 
-(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
+(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
 right.
 intro HP.
 assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
@@ -129,7 +129,7 @@ rewrite <- H0''. reflexivity.
 rewrite Heq.
 assumption.
 
-(* cases where P is true *)
+(** cases where P is true *)
 left; assumption.
 left; assumption.
 
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 5b7528be..4666d9b4 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -6,9 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: JMeq.v,v 1.8.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: JMeq.v,v 1.8.2.2 2004/08/03 17:42:32 herbelin Exp $ i*)
 
-(** John Major's Equality as proposed by C. Mc Bride *)
+(** John Major's Equality as proposed by C. Mc Bride
+
+  Reference:
+
+  [McBride] Elimination with a Motive, Proceedings of TYPES 2000,
+  LNCS 2277, pp 197-216, 2002.
+
+*)
 
 Set Implicit Arguments.
 
@@ -65,4 +72,4 @@ Lemma eq_dep_JMeq :
 Proof.
 destruct 1.
 apply JMeq_refl. 
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index ca7b760e..08873aa5 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RelationalChoice.v,v 1.3.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: RelationalChoice.v,v 1.3.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
 
-(* This file axiomatizes the relational form of the axiom of choice *)
+(** This file axiomatizes the relational form of the axiom of choice *)
 
 Axiom
   relational_choice :
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 78295591..7e361621 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ZArith.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
+(*i $Id: ZArith.v,v 1.5.2.2 2004/08/03 17:56:30 herbelin Exp $ i*)
 
 (** Library for manipulating integers based on binary encoding *)
 
@@ -19,4 +19,3 @@ Require Export Zsqrt.
 Require Export Zpower.
 Require Export Zdiv.
 Require Export Zlogarithm.
-Require Export Zbool.
\ No newline at end of file