aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287ef..3dfc85041 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl =
let expls_impl = compute_explicitable_implicit impl ty in
(ty, expls_impl, impl, compute_arguments_scope typ)
-let compute_internalization_env env ty =
+let compute_internalization_env env ?(impls=empty_internalization_env) ty =
List.fold_left3
(fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map)
- empty_internalization_env
+ impls
(**********************************************************************)
(* Contracting "{ _ }" in notations *)