diff options
Diffstat (limited to 'kernel/sign.mli')
| -rw-r--r-- | kernel/sign.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli index f4f26994f9..763a674716 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -9,7 +9,7 @@ open Term (* Signatures of named variables. *) -type 'a signature (* = [identifier list * 'a list] *) +type 'a signature val nil_sign : 'a signature val add_sign : (identifier * 'a) -> 'a signature -> 'a signature @@ -63,7 +63,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 type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature val gLOB : 'b signature -> ('b,'a) sign @@ -90,6 +90,8 @@ val number_of_rels : ('b,'a) sign -> int (* raise [Not_found] if the integer is out of range *) val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign +val make_all_name_different : ('a, 'b) sign -> ('a, 'b) sign + type ('b,'a) search_result = | GLOBNAME of identifier * 'b | RELNAME of int * 'a |