From 65ceda87c740b9f5a81ebf5a7873036c081b402c Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 29 Oct 2007 23:52:01 +0000 Subject: Revision of the FSetWeak Interface, so that it becomes a precise subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/OrderedType.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'theories/FSets/OrderedType.v') diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v index d59a9a354..ddee6c289 100644 --- a/theories/FSets/OrderedType.v +++ b/theories/FSets/OrderedType.v @@ -12,13 +12,6 @@ Require Export SetoidList. Set Implicit Arguments. Unset Strict Implicit. -(* TODO concernant la tactique order: - * propagate_lt n'est sans doute pas complet - * un propagate_le - * exploiter les hypotheses negatives restant a la fin - * faire que ca marche meme quand une hypothese depend d'un eq ou lt. -*) - (** * Ordered types *) Inductive Compare (X : Set) (lt eq : X -> X -> Prop) (x y : X) : Set := @@ -122,6 +115,13 @@ Module OrderedTypeFacts (O: OrderedType). intuition. Qed. +(* TODO concernant la tactique order: + * propagate_lt n'est sans doute pas complet + * un propagate_le + * exploiter les hypotheses negatives restant a la fin + * faire que ca marche meme quand une hypothese depend d'un eq ou lt. +*) + Ltac abstraction := match goal with (* First, some obvious simplifications *) | H : False |- _ => elim H -- cgit v1.2.3