diff options
| author | Pierre-Marie Pédrot | 2015-11-15 13:30:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-15 13:30:41 +0100 |
| commit | 7e7749ed22c328e041eb8ab59df5b6d32f777653 (patch) | |
| tree | bf4338e577fd43d1fb6985691226784e0ce57e1b /interp | |
| parent | f0ff590f380fb3d9fac6ebfdd6cfd7bf6874658e (diff) | |
| parent | 3aeb18bf1412a27309c39713e05eca2c27706ca8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
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 = []) = |