diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 5d03fbfd3..d74d21446 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -44,9 +44,11 @@ val eq_evar_info : evar_info -> evar_info -> bool val make_evar : named_context_val -> types -> evar_info val evar_concl : evar_info -> constr val evar_context : evar_info -> named_context +val evar_filtered_context : evar_info -> named_context val evar_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body val evar_filter : evar_info -> bool list +val evar_unfiltered_env : evar_info -> env val evar_env : evar_info -> env type evar_map @@ -208,6 +210,11 @@ val whd_sort_variable : evar_map -> constr -> constr val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map val define_sort_variable : evar_map -> sorts -> sorts -> evar_map +(**********************************************************) +(* Failure explanation *) + +type unsolvability_explanation = SeveralInstancesFound of int + (*********************************************************************) (* debug pretty-printer: *) |