diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-26 14:23:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-26 15:26:22 +0100 |
| commit | 29a5127dac6d4fbc317e38452cf0fe05916adc56 (patch) | |
| tree | adabfae9b7e860ef3e6aacb4b9f9f3871c6a71dc /pretyping/unification.mli | |
| parent | 1be28ac589a6affa81b905bbf223bdf520511a44 (diff) | |
Fixing destruct/induction with a using clause on a non-inductive type,
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 3b4998129..7f5cac2d2 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -65,8 +65,10 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> exception PatternNotFound +type prefix_of_inductive_support_flag = bool + type abstraction_request = -| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> |