diff options
Diffstat (limited to 'checker/declarations.mli')
| -rw-r--r-- | checker/declarations.mli | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/checker/declarations.mli b/checker/declarations.mli index 80c895bbe..cc3123ca7 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -30,16 +30,9 @@ type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted -(** Beware! In .vo files, lazy_constr are stored as integers - used as indexes for a separate table. The actual lazy_constr is restored - later, by [Safe_typing.LightenLibrary.load]. This allows us - to use here a different definition of lazy_constr than coqtop: - since the checker will inspect all proofs parts, even opaque - ones, no need to use Lazy.t here *) - type lazy_constr -val force_lazy_constr : lazy_constr -> constr -val lazy_constr_from_val : constr_substituted -> lazy_constr + +val indirect_opaque_access : (DirPath.t -> int -> constr) ref (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -63,7 +56,7 @@ type constant_body = { const_native_name : native_name ref; const_inline_code : bool } -val body_of_constant : constant_body -> constr_substituted option +val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool |