aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c754f1910c..8afe630ec5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -317,7 +317,7 @@ let rec it_mkGLambda loc2 env body =
let build_impls = function
|Implicit -> (function
|Name id -> Some (id, Impargs.Manual, (true,true))
- |Anonymous -> anomaly (Pp.str "Anonymous implicit argument"))
+ |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
|Explicit -> fun _ -> None
let impls_type_list ?(args = []) =