diff options
| author | Pierre-Marie Pédrot | 2016-06-22 20:31:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-24 15:16:03 +0200 |
| commit | e5446e385ba283f3c4cde83e0fc14987e500778a (patch) | |
| tree | ee89e4f3085899b043116b4ca90778a40fecbd21 | |
| parent | bd170eb3937aa55f665a671fe9d2916a26af2a09 (diff) | |
Optim in Clenv: use noccurn instead of depends.
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |