aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index bb3cbb6a8..6e63539ca 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -94,6 +94,7 @@ exception Occur
val occur_meta : Evd.evar_map -> constr -> bool
val occur_existential : Evd.evar_map -> constr -> bool
val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_in_decl :