diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 6 | ||||
| -rw-r--r-- | kernel/declareops.mli | 12 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.mli | 12 | ||||
| -rw-r--r-- | kernel/nativecode.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 6 |
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 |