Removing the generalization of the body of inductive schemes from

Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.

3 files changed, 6 insertions, 6 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c77ab06b9..ceb4facc1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = Term_typing.handle_entry_side_effects env ce in
+  let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
   assert(Declareops.side_effects_is_empty se);
   assert(Univ.ContextSet.is_empty ctx);
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5e0fb4dd3..4aa3c3bfd 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -153,7 +153,7 @@ val build_constant_by_tactic :
   types -> unit Proofview.tactic -> 
   Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> 
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index d1452fca2..16683d243 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -637,7 +637,7 @@ let make_bl_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal
     (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -759,7 +759,7 @@ let make_lb_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal
     (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx (* FIXME *)), eff
@@ -930,7 +930,7 @@ let make_eq_decidability mind =
   let ctx = Evd.empty_evar_universe_context (* FIXME *)in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in