diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 15:40:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 17:18:56 +0100 |
| commit | 7f427a8ab2e08e24c303cffd2e54d4fb477f3b00 (patch) | |
| tree | ce527d2b31a00ff6d06df5f178790c13c097b914 | |
| parent | cf4645acc78a8463fa533756efd9a8d9855d727d (diff) | |
Fixing #3997 (occur-check in the presence of primitive projections, patch
from Matthieu).
| -rw-r--r-- | pretyping/evarsolve.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5aa72c90a..921609aae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -186,6 +186,7 @@ let noccur_evar env evd evk c = (match pi2 (Environ.lookup_rel (i-k) env) with | None -> () | Some b -> occur_rec k (lift i b)) + | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c []) | _ -> iter_constr_with_binders succ occur_rec k c in try occur_rec 0 c; true with Occur -> false |