From dbde18a6eb9a8fca81a3e95209afdb8cfab4d26f Mon Sep 17 00:00:00 2001
From: courant
Date: Fri, 21 Apr 2000 08:47:57 +0000
Subject: Sign.db_signature is now an abstract type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@364 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/sign.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/sign.mli b/kernel/sign.mli
index 82d71fd4cb..ff53fca99a 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -54,7 +54,7 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 
 (*s Signatures with named and de Bruijn variables. *)
 
-type 'a db_signature = (name * 'a) list
+type 'a db_signature (* = [ (name * 'a) list ] *)
 type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
 
 val gLOB : 'b signature -> ('b,'a) sign
-- 
cgit v1.2.3