diff options
| author |  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-21 08:47:57 +0000 |
|---|---|---|
| committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-21 08:47:57 +0000 |
| commit | dbde18a6eb9a8fca81a3e95209afdb8cfab4d26f (patch) | |
| tree | f7c29ed190c2b2948d986ce6cc33aadbf04e5c28 /kernel/sign.mli | |
| parent | 9c6697d52b62221255830c22d62f16ce08797ddf (diff) | |
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
Diffstat (limited to 'kernel/sign.mli')
| -rw-r--r-- | kernel/sign.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli index 82d71fd4c..ff53fca99 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 |