diff options
| author | Gaëtan Gilbert | 2018-02-12 12:56:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 71b9ad8526155020c8451dd326a52e391a9a8585 (patch) | |
| tree | 48610b94a74a741e7c6f5ce46010404ebf0ce78f /kernel/cClosure.ml | |
| parent | 5cb337a0862e06a5b103b00c43cf9777e3468923 (diff) | |
Enable proof irrelevance for SProp.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index a29f3c6833..405d0b4223 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1194,12 +1194,12 @@ and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with | FLambda(_n,tys,f,e) -> - let (e',rvtys) = - List.fold_left (fun (e,ctxt) (na,ty) -> - (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) - (e,[]) tys in - let bd = kl info tab (mk_clos e' f) in - List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys + let (e',info,rvtys) = + List.fold_left (fun (e,info,ctxt) (na,ty) -> + (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt)) + (e,info,[]) tys in + let bd = kl info tab (mk_clos e' f) in + List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) |