diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 8a2974f6c8..9542dba9f8 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -90,3 +90,5 @@ val find_case_dep_nparams : val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool + +val keep_hyps : var_context -> Idset.t -> var_context |