diff options
| author | coqbot-app[bot] | 2020-08-31 12:09:18 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-31 12:09:18 +0000 |
| commit | daca83946ed5a001f2461fefa787a80f7dcdea01 (patch) | |
| tree | 0a746f4f5496290ca18c5d92d57cb7d3a9c89065 /interp/impargs.ml | |
| parent | b4ff2af4f43a2e0ba40c7f8a6260da1c75859045 (diff) | |
| parent | 8262041215c9bc3d13e768b1c422b52005083e85 (diff) | |
Merge PR #12875: Further extensions of About wrt Arguments and renaming
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'interp/impargs.ml')
| -rw-r--r-- | interp/impargs.ml | 10 |
1 files changed, 6 insertions, 4 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 |