diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 9 | ||||
| -rw-r--r-- | engine/termops.mli | 5 |
2 files changed, 13 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index f698f81513..ac8461a3ab 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -564,7 +564,14 @@ let occur_var_in_decl env hyp decl = occur_var env hyp typ || occur_var env hyp body -(* returns the list of free debruijn indices in a term *) +let local_occur_var id c = + let rec occur c = match kind_of_term c with + | Var id' -> if Id.equal id id' then raise Occur + | _ -> Constr.iter occur c + in + try occur c; false with Occur -> true + + (* returns the list of free debruijn indices in a term *) let free_rels m = let rec frec depth acc c = match kind_of_term c with 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] *) |