diff options
| author | Gaëtan Gilbert | 2020-09-21 13:35:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-09 11:48:46 +0200 |
| commit | cada5caf9c739efc7a2d932af4498b61f7fc9608 (patch) | |
| tree | 112cfdc602f5607a15027761ea7c4409e81296ca /pretyping/evardefine.mli | |
| parent | f53f84d32dff2820043df92e743234e3fdaa3520 (diff) | |
No bidirectionality when expected type for lambda is an evar.
This fixes #12623 (bidirectionality breaks impredicativity).
Diffstat (limited to 'pretyping/evardefine.mli')
| -rw-r--r-- | pretyping/evardefine.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index e5c3f8baa1..5702e169c8 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open EConstr open Evd open Environ @@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential -val split_tycon : - ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) - val split_as_array : env -> evar_map -> type_constraint -> evar_map * type_constraint (** If the constraint can be made to look like [array A] return [A], @@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t val pr_tycon : env -> evar_map -> type_constraint -> Pp.t +(** Used for bidi heuristic when typing lambdas. Transforms an applied + evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *) +val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t |