From e5446e385ba283f3c4cde83e0fc14987e500778a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 22 Jun 2016 20:31:01 +0200
Subject: Optim in Clenv: use noccurn instead of depends.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 78dce0d64c..853410db8b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -109,7 +109,7 @@ let clenv_environments evd bound t =
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) t2 in
+	  let dep = not (noccurn 1 t2) in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
-- 
cgit v1.2.3