From ec955042c050eb377fd5d46f95dafb36e5bd7d16 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Oct 2003 20:50:04 +0000
Subject: identity est equivalent sur Type (sauf sans argument)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4590 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 2d35928c54..33eb6a3221 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -42,7 +42,7 @@ Inductive Empty_set:Set :=.
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [refl_identity A a] *)
 
-Inductive identity [A:Set; a:A] : A->Set :=
+Inductive identity [A:Type; a:A] : A->Set :=
      refl_identity: (identity A a a).
 Hints Resolve refl_identity : core v62.
 
@@ -77,7 +77,6 @@ V7only [
 Notation Fst := (fst ? ?).
 Notation Snd := (snd ? ?).
 ].
-
 Hints Resolve pair inl inr : core v62.
 
 V7only[
-- 
cgit v1.2.3