diff options
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 3b49981290..7f5cac2d23 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 -> |