diff options
| author | Pierre-Marie Pédrot | 2015-11-11 18:45:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-11 18:45:32 +0100 |
| commit | 701a69732ef2abfc7384296e090a3e9bd7604bbd (patch) | |
| tree | 356247eb62159a080e343fef087a7cb705d6a0ea | |
| parent | ab1d8792143a05370a1efe3d19469c25b82d7097 (diff) | |
Fixing bug #3554: Anomaly: Anonymous implicit argument.
We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
| -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. |