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

4 files changed, 4 insertions, 19 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 47e56e3b03..33a26c8006 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -338,11 +338,6 @@ let cci_inductive locals env env_ar kind finite inds cst =
       Idset.empty inds
   in
   let hyps = keep_hyps env ids (named_context env) in
-  let inds' =
-    if Options.immediate_discharge then
-      List.map (abstract_inductive ntypes hyps) inds
-    else
-      inds in
   let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) =
     let recargs = listrec_mconstr env_ar ntypes params nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
@@ -373,7 +368,7 @@ let cci_inductive locals env env_ar kind finite inds cst =
       mind_params_ctxt = params }
   in
   let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
-  let packets = Array.of_list (list_map_i one_packet 1 inds') in
+  let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
     mind_hyps = sp_hyps;
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index c1e864523a..0191b63911 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -49,11 +49,8 @@ let instantiate_evar sign c args =
     replace_vars inst c
 
 let instantiate_constr sign c args =
-  if Options.immediate_discharge then
-    c
-  else
-    let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
-    instantiate sign c args
+  let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
+  instantiate sign c args
 
 let instantiate_type sign tty args =
   type_app (fun c -> instantiate_constr sign c args) tty
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;
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 0d7168c007..0899cf5e63 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -70,8 +70,7 @@ let instance_from_section_context sign =
     | [] -> [] in
   Array.of_list (inst_rec sign)
 let instance_from_section_context x =
-  if Options.immediate_discharge then [||]
-  else instance_from_section_context x
+  instance_from_section_context x
 
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)