From aa23fb72480182eddb7320ed59bf97448be7e04a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 May 2020 15:28:12 +0200
Subject: Termops: Adding functions local_occur_var_in_decl and
 occur_var_indirectly.

---
 engine/termops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 4e77aa9b3b..709fa361a9 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -92,12 +92,14 @@ 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_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
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
+val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool
 
 val free_rels : Evd.evar_map -> constr -> Int.Set.t
 
-- 
cgit v1.2.3