diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:23:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (patch) | |
| tree | 92587db07ddf50e2db16b270966115fa3d66d64a /pretyping/detyping.mli | |
| parent | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (diff) | |
[location] Switch glob_constr to Loc.located
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 4c6f9129f..84da3652f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -38,7 +38,7 @@ val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob val detype_case : bool -> (constr -> glob_constr) -> (constructor array -> bool list array -> constr array -> - (Loc.t * Id.t list * cases_pattern list * glob_constr) list) -> + (Id.t list * cases_pattern list * glob_constr) Loc.located list) -> (constr -> bool list -> bool) -> Id.t list -> inductive * case_style * bool list array * bool list -> constr option -> constr -> constr array -> glob_constr @@ -54,7 +54,9 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> cl val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit +(* XXX: This is a hack and should go away *) +val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit + val force_wildcard : unit -> bool val synthetize_type : unit -> bool |