diff options
author | 2001-10-11 17:27:20 +0000 | |
---|---|---|
committer | 2001-10-11 17:27:20 +0000 | |
commit | 301a70e45eac43f034077c95bce04edbcf2ab4ad (patch) | |
tree | d61c92f0d7a46203618a4610301c64d65c9c03ad /kernel/safe_typing.ml | |
parent | 1d5b3f16e202af2874181671abd86a47fca37cd7 (diff) |
Suppression option immediate_discharge; nettoyage de Declare et conséquences
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
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 6eba04182..a6ae51f89 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; |