diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /pretyping/detyping.mli | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 6c1e1265f..1e31e04d4 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -29,23 +29,23 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype : bool -> identifier list -> names_context -> constr -> glob_constr +val detype : bool -> Id.t list -> names_context -> constr -> glob_constr val detype_case : bool -> ('a -> glob_constr) -> (constructor array -> int array -> 'a array -> - (Loc.t * identifier list * cases_pattern list * glob_constr) list) -> + (Loc.t * Id.t list * cases_pattern list * glob_constr) list) -> ('a -> int -> bool) -> - identifier list -> inductive * case_style * int array * int -> + Id.t list -> inductive * case_style * int array * int -> 'a option -> 'a -> 'a array -> glob_constr val detype_sort : sorts -> glob_sort -val detype_rel_context : constr option -> identifier list -> names_context -> +val detype_rel_context : constr option -> Id.t list -> names_context -> rel_context -> glob_decl list (** look for the index of a named var or a nondep var as it is renamed *) -val lookup_name_as_displayed : env -> constr -> identifier -> int option +val lookup_name_as_displayed : env -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> constr -> int -> int option val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit |