diff options
| author | herbelin | 2000-05-22 19:54:35 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-22 19:54:35 +0000 |
| commit | 74263802c2aa7398b31bf5ddfcccaaddb46a45e4 (patch) | |
| tree | bdb5a965330590abc4460a21595f4478f0161fea /kernel/sign.mli | |
| parent | 08f5f4b1268624de1f8733ce30b51a62080f6ba6 (diff) | |
Renommage hypothèses de nom redondant dans les environnements
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@465 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |