diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-07 11:50:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-07 11:50:57 +0200 |
| commit | 3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch) | |
| tree | 34f2b0419b52861cb83bb42a90728161c7f792b4 /pretyping/unification.mli | |
| parent | d6175b9980808ff91f1299ca26a9a49a117169ca (diff) | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
Merge branch 'master' into econstr
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 6760283d2..148178f2f 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -71,14 +71,12 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool -type pending_constr = Evd.pending * constr - type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma + env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma type 'r abstraction_result = Names.Id.t * named_context_val * |