From f4f08411e85185cb03ea0ee0cb42c59988015e65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 24 Jun 2016 13:52:20 +0200
Subject: Optmimize the subst tactic.

Take advantage that the provided term is always a variable in Equality.is_eq_x.
---
 engine/termops.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

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
-- 
cgit v1.2.3