diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6eba041828..a6ae51f89f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -273,12 +273,6 @@ let add_global_declaration sp env locals (body,typ,cst) op = | Some b -> Idset.union (global_vars_set env b) (global_vars_set env typ) in let hyps = keep_hyps env ids (named_context env) in - let body, typ = - if Options.immediate_discharge then - option_app (fun c -> it_mkNamedLambda_or_LetIn c hyps) body, - it_mkNamedProd_or_LetIn typ hyps - else - body,typ in let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals, b, t)) hyps in let cb = { const_kind = kind_of_path sp; |