diff options
| author | barras | 2002-02-07 16:07:34 +0000 |
|---|---|---|
| committer | barras | 2002-02-07 16:07:34 +0000 |
| commit | 296faec482d17f9bfdc419f79ed565ecd8035e60 (patch) | |
| tree | 410123e747a8b3f3ca44aacb86f241c10360257a /pretyping/termops.mli | |
| parent | 85bdcf8b1ca9b515d848878537755069ed03fd27 (diff) | |
petit nettoyage de kernel/inductive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2a3e8b29ce..e47570f47e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -126,15 +126,15 @@ val names_of_rel_context : env -> names_context (* sets of free identifiers *) type used_idents = identifier list val occur_rel : int -> name list -> identifier -> bool -val occur_id : name list -> identifier -> constr -> bool +val occur_id : env -> name list -> identifier -> constr -> bool val next_name_not_occuring : - name -> identifier list -> name list -> constr -> identifier + env -> name -> identifier list -> name list -> constr -> identifier val concrete_name : - identifier list -> name list -> name -> + env -> identifier list -> name list -> name -> constr -> identifier option * identifier list val concrete_let_name : - identifier list -> name list -> + env -> identifier list -> name list -> name -> constr -> name * identifier list val global_vars : env -> constr -> identifier list val rename_bound_var : env -> identifier list -> types -> types |