Avoid type checking private_constants (side_eff) again during Qed (#4357).

Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing.  When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined.  Only when the
comparison is successful the private_constant is not re-checked.  Otherwise
else it is.  In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.

Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron).  Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.

11 files changed, 53 insertions, 52 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 8ac273c84..7a89b9f54 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -179,12 +179,12 @@ let build_beq_scheme mode kn =
       let rec aux c =
 	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
 	match kind_of_term c with
-        | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff
-        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff
+        | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants
         | Cast (x,_,_) -> aux (applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> 
-            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff
+            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
             else begin
               try
                 let eq, eff =
@@ -193,9 +193,8 @@ let build_beq_scheme mode kn =
                 let eqa, eff =
                   let eqa, effs = List.split (List.map aux a) in
                   Array.of_list eqa,
-                  Declareops.union_side_effects
-                    (Declareops.flatten_side_effects (List.rev effs))
-                    eff in
+                  List.fold_left Safe_typing.concat_private eff (List.rev effs)
+                  in
                 let args =
                   Array.append 
                     (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
@@ -238,7 +237,7 @@ let build_beq_scheme mode kn =
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (Lazy.force ff) in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
 	for i=0 to n-1 do
 	  let nb_cstr_args = List.length constrsi.(i).cs_args in
 	  let ar2 = Array.make n (Lazy.force ff) in
@@ -256,7 +255,7 @@ let build_beq_scheme mode kn =
                                           (nb_cstr_args+ndx+1)
                                           cc
                           in
-                          eff := Declareops.union_side_effects eff' !eff;
+                          eff := Safe_typing.concat_private eff' !eff;
                           Array.set eqs ndx
                               (mkApp (eqA,
                                 [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -288,7 +287,7 @@ let build_beq_scheme mode kn =
     let names = Array.make nb_ind Anonymous and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
         names.(i) <- Name (Id.of_string (rec_name i));
@@ -296,7 +295,7 @@ let build_beq_scheme mode kn =
                      (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
-        eff := Declareops.union_side_effects eff' !eff
+        eff := Safe_typing.concat_private eff' !eff
     done;
       (Array.init nb_ind (fun i ->
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
@@ -875,7 +874,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
     Not_found ->
       Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
-  let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
+  let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
   Tacticals.New.tclTHENLIST [
         Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
@@ -942,7 +941,7 @@ let make_eq_decidability mode mind =
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), Declareops.no_seff
+  ([|ans|], ctx), Safe_typing.empty_private_constants
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 805a29e39..e750f0ca2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let ctx = Evd.universe_context !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-	  (Entries.ParameterEntry 
+	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d75efeca1..433ef4dcc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+  Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
-      assert(Declareops.side_effects_is_empty sideff);
+      assert(Safe_typing.empty_private_constants = sideff);
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
@@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let ctx = Evd.universe_context ?names:pl evd in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let vars = Universes.universes_of_constr (List.hd fixdecls) in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 94b4af9dd..a031677b4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -26,17 +26,17 @@ val do_constraint : polymorphic ->
 
 (** {6 Hooks for Pcoq} *)
 
-val set_declare_definition_hook : (definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (definition_entry -> unit)
+val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
+val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
 
 (** {6 Definitions/Let} *)
 
 val interp_definition :
   lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
-  constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
+  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
-  definition_entry -> Impargs.manual_implicits ->
+  Safe_typing.private_constants definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind -> lident list option ->
@@ -170,4 +170,4 @@ val do_cofixpoint :
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
 val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 7d5d61fb8..b6da21e5a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -20,8 +20,8 @@ open Cooking
 (* Discharging mutual inductive *)
 
 let detype_param = function
-  | (Name id,None,p) -> id, Entries.LocalAssum p
-  | (Name id,Some p,_) -> id, Entries.LocalDef p
+  | (Name id,None,p) -> id, LocalAssum p
+  | (Name id,Some p,_) -> id, LocalDef p
   | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 218c47b28..dde801a7f 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -29,9 +29,9 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 type 'a scheme_kind = string
 
@@ -124,7 +124,9 @@ let define internal id c p univs =
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
   let entry = {
-    const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
+    const_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty),
+                       Safe_typing.empty_private_constants);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_polymorphic = p;
@@ -148,8 +150,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
-  const, Declareops.cons_side_effects
-     (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.add_private
+     (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -168,8 +170,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
-  Declareops.cons_side_effects 
-    (Safe_typing.sideff_of_scheme
+  Safe_typing.add_private 
+    (Safe_typing.private_con_of_scheme
       kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
@@ -181,10 +183,10 @@ let define_mutual_scheme kind mode names mind =
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Declareops.cons_side_effects
-      (Safe_typing.sideff_of_scheme
+  s, Safe_typing.add_private
+      (Safe_typing.private_con_of_scheme
             kind (Global.safe_env()) [ind, s])
-      Declareops.no_seff 
+      Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index d0844dd94..abd951c31 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -20,9 +20,9 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 (** Main functions to register a scheme builder *)
 
@@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind -> 
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> constant * Declareops.side_effects
+  Id.t option -> inductive -> constant * Safe_typing.private_constants
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
+  (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ae8ee7670..0b021254e 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma decl in
     (* let decltype = refresh_universes decltype in *)
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
     let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
@@ -469,7 +469,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
   ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
   fixpoint_message None [snd name]
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 665926922..e488f84f8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -541,7 +541,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff)
+let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
 
 let declare_mutual_definition l =
   let len = List.length l in
@@ -619,7 +619,7 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body else [], body, [||] 
       in
       let ce = 
-        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
+        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants);
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
 	  const_entry_polymorphic = poly;
@@ -796,12 +796,12 @@ let solve_by_tac name evi t poly ctx =
   let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
-  let entry = Term_typing.handle_entry_side_effects env entry in
-  let body, eff = Future.force entry.Entries.const_entry_body in
-  assert(Declareops.side_effects_is_empty eff);
+  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+  let body, eff = Future.force entry.const_entry_body in
+  assert(Safe_typing.empty_private_constants = eff);
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
-  (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx'
+  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 40f124ca3..61a8ee520 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,11 +17,11 @@ open Decl_kinds
 
 (** Forward declaration. *)
 val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
   (Id.t -> definition_kind ->
-     Entries.definition_entry -> Impargs.manual_implicits
+     Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
 val check_evars : env -> evar_map -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 60fe76bb8..b1be4c92a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -160,8 +160,8 @@ let degenerate_decl (na,b,t) =
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
   match b with
-    | None -> (id, Entries.LocalAssum t)
-    | Some b -> (id, Entries.LocalDef b)
+    | None -> (id, LocalAssum t)
+    | Some b -> (id, LocalDef b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -297,7 +297,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	        try
 		  let entry = {
 		    const_entry_body =
-		      Future.from_val (Term_typing.mk_pure_proof proj);
+		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;