diff options
| author | Hugo Herbelin | 2015-02-24 14:22:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-24 16:00:19 +0100 |
| commit | 2734891ab7e90c5b488416d11c3dc41c224773e7 (patch) | |
| tree | d0658a42aabb70d0f4ae698647f67963b5885e8b | |
| parent | def8cafc0ceae48d57a44ae120730ea36cb56b88 (diff) | |
Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on
integrating ensure_evar_independent into is_constrainable_in.
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9f1b118fb3..13c63e9784 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1027,7 +1027,7 @@ let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t = let params = fst (Array.chop n args) in Array.for_all (is_constrainable_in false force env evd k g) params | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args - | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2 + | Prod (na,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force (push_rel (na,None,t1) env) evd k g t2 | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels |