diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | checker/cic.mli | 4 | ||||
| -rw-r--r-- | checker/declarations.ml | 7 |
3 files changed, 8 insertions, 4 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index cd858000a4..24479fb8a9 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -21,6 +21,7 @@ CList CString CArray Util +Future CUnix System Envars diff --git a/checker/cic.mli b/checker/cic.mli index d55a9d5c06..fd33516748 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -181,14 +181,14 @@ type inline = int option type constant_def = | Undef of inline | Def of constr_substituted - | OpaqueDef of lazy_constr + | OpaqueDef of lazy_constr Future.computation type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints; + const_constraints : Univ.constraints Future.computation; const_native_name : native_name ref; const_inline_code : bool } diff --git a/checker/declarations.ml b/checker/declarations.ml index 58a5f26020..0981cfd1a8 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -434,12 +434,15 @@ let force_lazy_constr = function let subst_constant_def sub = function | Undef inl -> Undef inl | Def c -> Def (subst_constr_subst sub c) - | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + | OpaqueDef lc -> + OpaqueDef (Future.from_val (subst_lazy_constr sub (Future.join lc))) + +type constant_constraints = Univ.constraints Future.computation let body_of_constant cb = match cb.const_body with | Undef _ -> None | Def c -> Some (force_constr c) - | OpaqueDef c -> Some (force_lazy_constr c) + | OpaqueDef c -> Some (force_lazy_constr (Future.join c)) let constant_has_body cb = match cb.const_body with | Undef _ -> false |