diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 13 | ||||
| -rw-r--r-- | engine/termops.mli | 6 |
2 files changed, 16 insertions, 3 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index d60aa69ccb..a0248fa01b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -839,6 +839,16 @@ let occur_var env sigma id c = in try occur_rec c; false with Occur -> true +let occur_vars env sigma ids c = + let rec occur_rec c = + match EConstr.destRef sigma c with + | gr, _ -> + let vars = vars_of_global env gr in + if not (Id.Set.is_empty (Id.Set.inter ids vars)) then raise Occur + | exception DestKO -> EConstr.iter sigma occur_rec c + in + try occur_rec c; false with Occur -> true + exception OccurInGlobal of GlobRef.t let occur_var_indirectly env sigma id c = @@ -853,6 +863,9 @@ let occur_var_indirectly env sigma id c = let occur_var_in_decl env sigma hyp decl = NamedDecl.exists (occur_var env sigma hyp) decl +let occur_vars_in_decl env sigma hyps decl = + NamedDecl.exists (occur_vars env sigma hyps) decl + let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with | Var id' -> if Id.equal id id' then raise Occur diff --git a/engine/termops.mli b/engine/termops.mli index bdde2c450d..0faebecb1b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -89,9 +89,9 @@ 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_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option -val occur_var_in_decl : - env -> Evd.evar_map -> - Id.t -> named_declaration -> bool +val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool +val occur_vars : env -> Evd.evar_map -> Id.Set.t -> constr -> bool +val occur_vars_in_decl : env -> Evd.evar_map -> Id.Set.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool |