From 10fa54f60acdfc8de6b59659f9fa8bc1ed3c18e6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 28 May 2006 16:21:04 +0000 Subject: - Déplacement des types paramétriques prod, sum, option, identity, sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bvector.v | 24 ++++++++++++------------ theories/Bool/DecBool.v | 4 ++-- 2 files changed, 14 insertions(+), 14 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index eafc1fabb..1c965c7e0 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -46,9 +46,9 @@ Une fonction binaire sur A génère une fonction des couple de vecteurs de taille n dans les vecteurs de taille n en appliquant f terme à terme. *) -Variable A : Set. +Variable A : Type. -Inductive vector : nat -> Set := +Inductive vector : nat -> Type := | Vnil : vector 0 | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). @@ -59,7 +59,7 @@ Defined. Definition Vtail : forall n:nat, vector (S n) -> vector n. Proof. - intros n v; inversion v; exact H0. + intros n v; inversion v as [|_ n0 H0 H1]; exact H0. Defined. Definition Vlast : forall n:nat, vector (S n) -> A. @@ -68,7 +68,7 @@ Proof. inversion v. exact a. - inversion v. + inversion v as [| n0 a H0 H1]. exact (f H0). Defined. @@ -85,7 +85,7 @@ Proof. induction n as [| n f]; intro v. exact Vnil. - inversion v. + inversion v as [| a n0 H0 H1]. exact (Vcons a n (f H0)). Defined. @@ -94,7 +94,7 @@ Proof. induction n as [| n f]; intros a v. exact (Vcons a 0 v). - inversion v. + inversion v as [| a0 n0 H0 H1 ]. exact (Vcons a (S n) (f a H0)). Defined. @@ -104,7 +104,7 @@ Proof. inversion v. exact (Vcons a 1 v). - inversion v. + inversion v as [| a n0 H0 H1 ]. exact (Vcons a (S (S n)) (f H0)). Defined. @@ -128,7 +128,7 @@ Proof. induction n as [| n f]; intros p v v0. simpl in |- *; exact v0. - inversion v. + inversion v as [| a n0 H0 H1]. simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). Defined. @@ -139,7 +139,7 @@ Proof. induction n as [| n g]; intro v. exact Vnil. - inversion v. + inversion v as [| a n0 H0 H1]. exact (Vcons (f a) n (g H0)). Defined. @@ -150,15 +150,15 @@ Proof. induction n as [| n h]; intros v v0. exact Vnil. - inversion v; inversion v0. + inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3]. exact (Vcons (g a a0) n (h H0 H2)). Defined. Definition Vid : forall n:nat, vector n -> vector n. Proof. -destruct n; intros. +destruct n; intro X. exact Vnil. -exact (Vcons (Vhead _ H) _ (Vtail _ H)). +exact (Vcons (Vhead _ X) _ (Vtail _ X)). Defined. Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v). diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 7fa518d66..82363fff7 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -10,7 +10,7 @@ Set Implicit Arguments. -Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C := +Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := if H then x else y. @@ -28,4 +28,4 @@ intros; case H; auto. intro; absurd A; trivial. Qed. -Unset Implicit Arguments. \ No newline at end of file +Unset Implicit Arguments. -- cgit v1.2.3