From 29a5127dac6d4fbc317e38452cf0fe05916adc56 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 26 Oct 2014 14:23:00 +0100 Subject: 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". --- pretyping/unification.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/unification.mli') 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 -> -- cgit v1.2.3