- 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


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 14 deletions

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.