diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c754f191..a7b1bb41 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 = []) = |