diff options
author | 2016-06-24 13:52:20 +0200 | |
---|---|---|
committer | 2016-06-24 15:16:03 +0200 | |
commit | f4f08411e85185cb03ea0ee0cb42c59988015e65 (patch) | |
tree | 2832b87b02e05114aec2b8ce888448249d0aee76 /engine/termops.mli | |
parent | e5446e385ba283f3c4cde83e0fc14987e500778a (diff) |
Optmimize the subst tactic.
Take advantage that the provided term is always a variable in Equality.is_eq_x.
Diffstat (limited to 'engine/termops.mli')
-rw-r--r-- | engine/termops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 76a31037b..5d85088f8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -96,6 +96,7 @@ val strip_head_cast : constr -> constr val drop_extra_implicit_args : constr -> constr (** occur checks *) + exception Occur val occur_meta : types -> bool val occur_existential : types -> bool @@ -105,6 +106,10 @@ val occur_var : env -> Id.t -> types -> bool val occur_var_in_decl : env -> Id.t -> Context.Named.Declaration.t -> bool + +(** As {!occur_var} but assume the identifier not to be a section variable *) +val local_occur_var : Id.t -> types -> bool + val free_rels : constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) |