diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index fc227b5fb2..24e605ef4d 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -231,6 +231,8 @@ val fold_named_context_both_sides : named_context -> init:'a -> 'a val mem_named_context : identifier -> named_context -> bool +val clear_named_body : identifier -> env -> env + val global_vars : env -> constr -> identifier list val global_vars_set_of_decl : env -> named_declaration -> Idset.t |