diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:18:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:18:41 +0000 |
| commit | 87ab5e4f9a4f93d152df721f97a0bcb6cddef973 (patch) | |
| tree | 53f9e45dc0a5d10f180af85876f45b3cf27ba266 /pretyping/termops.mli | |
| parent | 090b29f754f44882a49961764e63be18f0d356c4 (diff) | |
Changement de l'afficheur pour que les variables liées aient un nom indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9031ec42d..0f970706a 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -151,16 +151,15 @@ val add_vname : Idset.t -> name -> Idset.t (* sets of free identifiers *) type used_idents = identifier list val occur_rel : int -> name list -> identifier -> bool -val occur_id : env -> name list -> identifier -> constr -> bool +val occur_id : name list -> identifier -> constr -> bool val next_name_not_occuring : - env -> name -> identifier list -> name list -> constr -> identifier + bool -> name -> identifier list -> name list -> constr -> identifier val concrete_name : - env -> identifier list -> name list -> name -> - constr -> identifier option * identifier list + bool -> identifier list -> name list -> name -> constr -> + name * identifier list val concrete_let_name : - env -> identifier list -> name list -> - name -> constr -> name * identifier list + bool -> identifier list -> name list -> name -> constr -> name * identifier list val rename_bound_var : env -> identifier list -> types -> types (* other signature iterators *) |