diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 4f47bfd886..b935efd8c6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -64,6 +64,7 @@ val apply_rel_list : val check_fix : env -> 'a evar_map -> constr -> unit val check_cofix : env -> 'a evar_map -> constr -> unit +val control_only_guard : env -> 'a evar_map -> constr -> unit val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array -> unsafe_judgment array -> constraints |