aboutsummaryrefslogtreecommitdiff
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b6816dd484..3c9e1cac54 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -70,12 +70,12 @@ let lookup_module mp env =
let mk_mtb mp sign delta =
{ mod_mp = mp;
- mod_expr = Abstract;
+ mod_expr = ();
mod_type = sign;
mod_type_alg = None;
mod_constraints = Univ.ContextSet.empty;
mod_delta = delta;
- mod_retroknowledge = []; }
+ mod_retroknowledge = ModTypeRK; }
let rec check_module env mp mb =
let (_:module_signature) =