Optmimize the subst tactic.

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

3 files changed, 20 insertions, 6 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] *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 17b44fbcc8..35be1fcb6e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1663,10 +1663,14 @@ exception FoundHyp of (Id.t * constr * bool)
 let is_eq_x gl x d =
   let id = get_id d in
   try
+    let is_var id c = match kind_of_term c with
+    | Var id' -> Id.equal id id'
+    | _ -> false
+    in
     let c = pf_nf_evar gl (get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
-    if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1713,14 +1717,12 @@ let subst_one_var dep_proof_ok x =
     let xval = pf_get_hyp x gl |> get_value in
     (* If x has a body, simply replace x with body and clear x *)
     if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
-      (* x is a variable: *)
-      let varx = mkVar x in
       (* Find a non-recursive definition for x *)
       let res =
         try
           (** [is_eq_x] ensures nf_evar on its side *)
           let hyps = Proofview.Goal.hyps gl in
-          let test hyp _ = is_eq_x gl varx hyp in
+          let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
           errorlabstrm "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++