diff options
| author | Matthieu Sozeau | 2017-07-27 16:10:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:52:39 +0100 |
| commit | 46b671c7473385ec7747a796e85b3cf704d000c6 (patch) | |
| tree | 7f340874881d5c2d266f1f39de145bd7d95af49c /engine/evarutil.mli | |
| parent | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (diff) | |
Evd/evarsolve: add an abstraction field to evars for unification
Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 23b240f1a0..bb0da44103 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -42,7 +42,7 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> @@ -50,7 +50,7 @@ val new_evar : val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> @@ -80,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> |