Parameterize the constant_body type by opaque subproofs.

10 files changed, 24 insertions, 24 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 19da63b4d4..d879f4ee95 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -152,7 +152,7 @@ let abstract_constant_body c (hyps, subst) =
   let c = Vars.subst_vars subst c in
   it_mkLambda_or_LetIn c hyps
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result = {
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index d218dd36da..ffd4e51ffc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -13,7 +13,7 @@ open Declarations
 
 (** {6 Cooking the constants. } *)
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 649bb8725d..36ee952099 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,9 +87,9 @@ type typing_flags = {
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaqueDef *)
-type constant_body = {
+type 'opaque constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
-    const_body : (Constr.t Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+    const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
@@ -246,7 +246,7 @@ type module_alg_expr =
 (** A component of a module structure *)
 
 type structure_field_body =
-  | SFBconst of constant_body
+  | SFBconst of Opaqueproof.opaque constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 54a853fc81..fb02c6a029 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
 
 (** {6 Constants} *)
 
-val subst_const_body : substitution -> constant_body -> constant_body
+val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body
 
 (** Is there a actual body in const_body ? *)
 
-val constant_has_body : constant_body -> bool
+val constant_has_body : 'a constant_body -> bool
 
-val constant_polymorphic_context : constant_body -> AUContext.t
+val constant_polymorphic_context : 'a constant_body -> AUContext.t
 
 (** Is the constant polymorphic? *)
-val constant_is_polymorphic : constant_body -> bool
+val constant_is_polymorphic : 'a constant_body -> bool
 
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val is_opaque : constant_body -> bool
+val is_opaque : 'a constant_body -> bool
 
 (** {6 Inductive types} *)
 
@@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
     of the structure, but simply hash-cons all inner constr
     and other known elements *)
 
-val hcons_const_body : constant_body -> constant_body
+val hcons_const_body : 'a constant_body -> 'a constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
 val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 97c9f8654a..67125e9ad1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,7 +46,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8c6bc105c7..6d3756e891 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -42,7 +42,7 @@ type link_info =
 
 type key = int CEphemeron.key option ref
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
@@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env
 val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
-val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
-val add_constant : Constant.t -> constant_body -> env -> env
-val add_constant_key : Constant.t -> constant_body -> link_info ->
+val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env
+val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info ->
   env -> env
 val lookup_constant_key :  Constant.t -> env -> constant_key
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
-val lookup_constant    : Constant.t -> env -> constant_body
+val lookup_constant    : Constant.t -> env -> Opaqueproof.opaque constant_body
 val evaluable_constant : Constant.t -> env -> bool
 
 (** New-style polymorphism *)
@@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
-val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 96efa7faa5..b5c03b6ca3 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val empty_updates : code_location_updates
 val register_native_file : string -> unit
 
 val compile_constant_field : env -> string -> Constant.t ->
-  global list -> constant_body -> global list
+  global list -> 'a constant_body -> global list
 
 val compile_mind_field : ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f2e7cff8ec..36f1515a8c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -247,7 +247,7 @@ let get_opaque_body env cbo =
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : Declarations.constant_body;
+  seff_body : Opaqueproof.opaque Declarations.constant_body;
   seff_env : seff_env;
   seff_role : Entries.side_effect_role;
 }
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1857ea3329..24845ce459 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -31,7 +31,7 @@ open Mod_subst
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
 type namedobject =
-  | Constant of constant_body
+  | Constant of Opaqueproof.opaque constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1fa5eca2e3..01b69b2b66 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,9 +33,9 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
-    constant_body
+    Opaqueproof.opaque constant_body
 
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
@@ -43,4 +43,4 @@ val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  Constant.t -> env -> Cooking.result -> constant_body
+  Constant.t -> env -> Cooking.result -> Opaqueproof.opaque constant_body