diff options
| author | herbelin | 2008-10-19 16:15:12 +0000 |
|---|---|---|
| committer | herbelin | 2008-10-19 16:15:12 +0000 |
| commit | cddb721edc8c2e61b29a64349cd199c0dfce3d11 (patch) | |
| tree | 37d3e221e4402214c63f2bffa46ff9e0152f41c1 /theories | |
| parent | add39fd4566c0e00293c2082077d08fb21178607 (diff) | |
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
- Extension du test de réversibilité acyclique des notations dures aux
notations de type abbréviation (du genre inhabited A := A).
- Ajout options Local/Global à Transparent/Opaque.
- Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé
dependent retiré).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 2 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 2 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 8555886023..dad60fb779 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -21,7 +21,7 @@ Set Implicit Arguments. Require Export Classical. Require Import ChoiceFacts. -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Axiom constructive_definite_description : forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 6673fa8c96..d4ba4a3a7b 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -119,7 +119,7 @@ Qed. *) -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Lemma prop_ext_A_eq_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index b96ae30e4e..95a07f2f3c 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Section ExtensionalEpsilon_imp_EM. |