diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 27e964b6a..c48c97910 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -172,7 +172,11 @@ val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds val pr_tycon : env -> type_constraint -> Pp.std_ppcmds -(**********************************) -(* Removing hyps in evars'context *) +(*********************************************************************) +(* Removing hyps in evars'context; *) +(* raise OccurHypInSimpleClause if the removal breaks dependencies *) + +exception OccurHypInSimpleClause of identifier * identifier option + val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types -> identifier list -> named_context_val * types |