Merge branch 'v8.5'

7 files changed, 32 insertions, 28 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e6a8cbe3ad..8a6d93cf7c 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
     let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
-      (c, Evd.evar_universe_context sigma), Declareops.no_seff
+      (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
  
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f7d3ad5d0a..b2603315d5 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -193,7 +193,7 @@ let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
   (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Declareops.no_seff)
+      (c, ctx), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff
+  in (c, Evd.evar_universe_context_of ctx),
+      Safe_typing.concat_private eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun _ ind -> fix_r2l_forward_rew_scheme
-     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -704,7 +705,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants)
 
 (* End of rewriting schemes *)
 
@@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind =
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
     (* May fail if equality is not defined *)
-    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
+    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 6bb84808a9..3fe3307308 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
 val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> 
   constr Evd.in_evar_universe_context
 val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> 
-  constr Evd.in_evar_universe_context * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
 val sym_scheme_kind : individual scheme_kind
 
 val build_sym_involutive_scheme : env -> inductive -> 
-  constr Evd.in_evar_universe_context * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 85bc50216e..56878f1125 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -318,7 +318,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let sigma, elim = Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c) in
-	sigma, elim, Declareops.no_seff
+	sigma, elim, Safe_typing.empty_private_constants
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 04a78dc574..75e69bc091 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -230,7 +230,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
+  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
+			       ~univs:(snd ctx) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 648d68f276..d1b14e3d99 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1810,9 +1810,9 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
+  let pl, ctx = Evd.universe_context sigma in
   let cst = 
-    Declare.definition_entry ~types:typ ~poly
-      ~univs:(Evd.universe_context sigma) term
+    Declare.definition_entry ~types:typ ~poly ~univs:ctx term
   in
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 94e334914c..289d5109a5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2514,11 +2514,13 @@ let bring_hyps hyps =
   else
     Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
+      let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
       Proofview.Refine.refine { run = begin fun sigma ->
-        let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in
+        let Sigma (ev, sigma, p) =
+          Evarutil.new_evar env sigma ~principal:true ~store newcl in
         Sigma (mkApp (ev, args), sigma, p)
       end }
     end }
@@ -4555,9 +4557,9 @@ let abstract_subproof id gk tac =
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
   let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
   let evd = Evd.set_universe_context evd ectx in
-  let open Declareops in
-  let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
-  let effs = cons_side_effects eff
+  let open Safe_typing in
+  let eff = private_con_of_con (Global.safe_env ()) cst in
+  let effs = add_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>