diff options
| author | Matthieu Sozeau | 2015-02-12 22:41:40 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-02-12 22:43:00 +0100 |
| commit | 5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf (patch) | |
| tree | 5ea51c592bbf3304d1e54616a27313780055892c /interp | |
| parent | 43471abd4e61e7528fdaa2c576e7cb825a203c13 (diff) | |
Univs: fix bug #3978: carry around the universe context used to
typecheck with definitions and thread it accordingly when typechecking
module expressions.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/modintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index fdc6e609bc..bf0b2f9800 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,7 +61,9 @@ let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> - WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*) + let c, ectx = interp_constr env (Evd.from_env env) c in + let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in + WithDef (fqid,(c,ctx)) let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc |