diff options
Diffstat (limited to 'kernel')
| -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 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 |