diff options
| author | Pierre-Marie Pédrot | 2016-06-24 21:23:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-24 21:24:39 +0200 |
| commit | a553126c9e0984f38b1a15f2db60458813a177c9 (patch) | |
| tree | 3a493b094eeb86d741a38836563f40aa0798d4ed /engine/termops.mli | |
| parent | 922ad0c1cb4a4badf4c9c2cd098285a008495519 (diff) | |
| parent | 4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff) | |
Several easy but efficient optimizations for subst and clear tactics.
They were spotted by profiling tactics manipulating huge terms, provided by
Jason Gross.
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 76a31037bc..5d85088f8d 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] *) |