Optmimize the subst tactic.

Take advantage that the provided term is always a variable in Equality.is_eq_x.

2 files changed, 13 insertions, 1 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index f698f8151..ac8461a3a 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 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] *)