diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index d55a9d5c0..fd3351674 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 } |