diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/sign.ml | 8 | ||||
| -rw-r--r-- | kernel/sign.mli | 6 |
2 files changed, 12 insertions, 2 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index 00a160ffd6..fb2c8d31d2 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -243,6 +243,14 @@ let lookup_id id env = with | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) +let make_all_name_different (ENVIRON((dom,_) as sign,dbs)) = + let _,newdbs = + List.fold_right + (fun (na,t) (avoid,newdbs) -> + let id = next_name_away na avoid in + (id::avoid),((Name id,t)::newdbs)) + dbs (dom,[]) + in ENVIRON (sign,newdbs) type 'b assumptions = (typed_type,'b) sign type context = (typed_type,typed_type) sign 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 |