diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 59f7750d3f..44a96b613c 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -109,6 +109,7 @@ val free_rels : constr -> Intset.t val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val collect_metas : constr -> int list +val collect_visible_vars : constr -> identifier list val occur_term : constr -> constr -> bool (* Synonymous of dependent *) (* Substitution of metavariables *) |