diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3554.v | 1 |
2 files changed, 2 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 = []) = diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v new file mode 100644 index 0000000000..13a79cc840 --- /dev/null +++ b/test-suite/bugs/closed/3554.v @@ -0,0 +1 @@ +Example foo (f : forall {_ : Type}, Type) : Type. |