diff options
| author | Hugo Herbelin | 2020-08-22 12:48:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (patch) | |
| tree | ad1bc6c93d8d914d09724a19561baa1899d4e7b9 /interp | |
| parent | 3df82e1adcfb96320b3fbbb622d9e54cb0a176e1 (diff) | |
When reporting an implicit argument error on a rename argument, use the renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.ml | 10 | ||||
| -rw-r--r-- | interp/impargs.mli | 2 |
2 files changed, 7 insertions, 5 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index 48961c6c8a..7742f985de 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -667,10 +667,12 @@ let explicit_kind i = function let compute_implicit_statuses autoimps l = let rec aux i = function - | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | na :: autoimps, MaxImplicit :: manualimps -> + | _ :: autoimps, (_, Explicit) :: manualimps -> None :: aux (i+1) (autoimps, manualimps) + | na :: autoimps, (Anonymous, MaxImplicit) :: manualimps + | _ :: autoimps, (na, MaxImplicit) :: manualimps -> Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | na :: autoimps, NonMaxImplicit :: manualimps -> + | na :: autoimps, (Anonymous, NonMaxImplicit) :: manualimps + | _ :: autoimps, (na, NonMaxImplicit) :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality Error na i imps' false in Some (explicit_kind i na, Manual, (max, true)) :: imps' @@ -693,7 +695,7 @@ let set_implicits local ref l = check_rigidity (is_rigid env sigma t); (* Sort by number of implicits, decreasing *) let is_implicit = function - | Explicit -> false + | _, Explicit -> false | _ -> true in let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in diff --git a/interp/impargs.mli b/interp/impargs.mli index 97841b37f2..c8bcef19c8 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -117,7 +117,7 @@ val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> (** [set_implicits local ref l] Manual declaration of implicit arguments. `l` is a list of possible sequences of implicit statuses. *) -val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit +val set_implicits : bool -> GlobRef.t -> (Name.t * Glob_term.binding_kind) list list -> unit val implicits_of_global : GlobRef.t -> implicits_list list |