diff options
| -rw-r--r-- | kernel/cClosure.ml | 2 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 2 | ||||
| -rw-r--r-- | kernel/cbytegen.mli | 2 | ||||
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 6 | ||||
| -rw-r--r-- | pretyping/cbv.ml | 2 |
7 files changed, 9 insertions, 9 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 412637c4b6..95f88c0306 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -389,7 +389,7 @@ type clos_infos = { i_flags : reds; i_cache : infos_cache } -type clos_tab = fconstr constant_def KeyTable.t +type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index b1b69dded8..1a790eaed6 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def +val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 6a9550342c..bdaf5fe422 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -20,7 +20,7 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> universes -> Constr.t Mod_subst.substituted constant_def -> + env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9b974c4ecc..19da63b4d4 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = { - cook_body : constr Mod_subst.substituted constant_def; + cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def; cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index b0f143c47d..d218dd36da 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,7 +18,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = { - cook_body : constr Mod_subst.substituted constant_def; + cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def; cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5551742c02..649bb8725d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,10 +47,10 @@ type inline = int option transparent body, or an opaque one *) (* Global declarations (i.e. constants) can be either: *) -type 'a constant_def = +type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) - | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) + | OpaqueDef of 'opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) type universes = @@ -89,7 +89,7 @@ type typing_flags = { * the OpaqueDef *) type constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) - const_body : Constr.t Mod_subst.substituted constant_def; + const_body : (Constr.t Mod_subst.substituted, Opaqueproof.opaque) constant_def; const_type : types; const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index c9f18d89be..5ea9b79336 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -145,7 +145,7 @@ let mkSTACK = function type cbv_infos = { env : Environ.env; - tab : cbv_value Declarations.constant_def KeyTable.t; + tab : (cbv_value, Empty.t) Declarations.constant_def KeyTable.t; reds : RedFlags.reds; sigma : Evd.evar_map } |