From ed4d62c2a4ef8cc6796dfa03662900be67339ff9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jul 2014 17:42:50 +0200 Subject: make a few lines fit the screen --- kernel/term_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index da0326981..843d8f8a3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -162,7 +162,7 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body, ctx), side_eff) -> + Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> let body = handle_side_effects env body side_eff in let env' = push_context_set ctx env in let j = infer env' body in -- cgit v1.2.3