From c511207bd0f25c4199770233175924a725526bd3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 15 Dec 2013 14:47:20 +0000
Subject: Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4.
 VERSION: bump version number.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Axioms.v | 40 +++++++++++++++++-----------------------
 1 file changed, 17 insertions(+), 23 deletions(-)

(limited to 'lib')

diff --git a/lib/Axioms.v b/lib/Axioms.v
index 52a7fff..6ae8669 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.v
@@ -16,44 +16,38 @@
 (** This file collects some axioms used throughout the CompCert development. *)
 
 Require ClassicalFacts.
+Require FunctionalExtensionality.
 
 (** * Extensionality axioms *)
 
-(** The following [Require Export] gives us functional extensionality for dependent function types:
-<<
-Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, 
-  forall (f g : forall x : A, B x), 
-  (forall x, f x = g x) -> f = g.
->> 
-and, as a corollary, functional extensionality for non-dependent functions:
-<<
-Lemma functional_extensionality {A B} (f g : A -> B) : 
+(** The [Require FunctionalExtensionality] gives us functional
+    extensionality for dependent function types: *)
+
+Lemma functional_extensionality_dep:
+  forall {A: Type} {B : A -> Type} (f g : forall x : A, B x),
   (forall x, f x = g x) -> f = g.
->>
+Proof @FunctionalExtensionality.functional_extensionality_dep.
+
+(** and, as a corollary, functional extensionality for non-dependent functions:
 *)
-Require Export FunctionalExtensionality.
+
+Lemma functional_extensionality:
+  forall {A B: Type} (f g : A -> B), (forall x, f x = g x) -> f = g.
+Proof @FunctionalExtensionality.functional_extensionality.
 
 (** For compatibility with earlier developments, [extensionality]
   is an alias for [functional_extensionality]. *)
 
 Lemma extensionality:
   forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
-Proof. intros; apply functional_extensionality. auto. Qed.
+Proof @functional_extensionality.
 
 Implicit Arguments extensionality.
 
-(** We also assert propositional extensionality. *)
-
-Axiom prop_ext: ClassicalFacts.prop_extensionality.
-Implicit Arguments prop_ext.
-
 (** * Proof irrelevance *)
 
-(** We also use proof irrelevance, which is a consequence of propositional
-    extensionality. *)
+(** We also use proof irrelevance. *)
+
+Axiom proof_irr: ClassicalFacts.proof_irrelevance.
 
-Lemma proof_irr: ClassicalFacts.proof_irrelevance.
-Proof.
-  exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext).
-Qed.
 Implicit Arguments proof_irr.
-- 
cgit v1.2.3