aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/modintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/modintern.ml')
-rw-r--r--interp/modintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 2d81194f2..c8a42c293 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,7 +61,7 @@ let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
WithMod (fqid,lookup_module qid)
| CWith_Definition ((_,fqid),c) ->
- WithDef (fqid,fst (interp_constr Evd.empty env c)) (*FIXME*)
+ WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*)
let loc_of_module = function
| CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc