Merge PR #10202: Slightly more robust manual implicit arguments

Reviewed-by: ejgallego

1 files changed, 15 insertions, 12 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2aa002ead1..df28b32f81 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
 open EConstr
 open Reductionops
 open Namegen
+open Constrexpr
 
 module NamedDecl = Context.Named.Declaration
 
@@ -289,7 +290,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal
 
 type implicit_status =
     (* None = Not implicit *)
-    (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
+    (explicitation * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
 
@@ -299,9 +300,12 @@ let is_status_implicit = function
   | None -> false
   | _ -> true
 
+let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+
 let name_of_implicit = function
   | None -> anomaly (Pp.str "Not an implicit argument.")
-  | Some (id,_,_) -> id
+  | Some (ExplByName id,_,_) -> id
+  | Some (ExplByPos (k,_),_,_) -> name_of_pos k
 
 let maximal_insertion_of = function
   | Some (_,_,(b,_)) -> b
@@ -336,7 +340,7 @@ let rec prepare_implicits f = function
   | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
   | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
-      Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+      Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
 let set_manual_implicits flags enriching autoimps l =
@@ -346,15 +350,14 @@ let set_manual_implicits flags enriching autoimps l =
        let imps' = merge (k+1) autoimps explimps in
        begin match autoimp, explimp.CAst.v with
        | (Name id,_), Some (_,max) ->
-          Some (id, Manual, (set_maximality imps' max, true))
+          Some (ExplByName id, Manual, (set_maximality imps' max, true))
        | (Name id,Some exp), None when enriching ->
-          Some (id, exp, (set_maximality imps' flags.maximal, true))
+          Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
        | (Name _,_), None -> None
        | (Anonymous,_), Some (Name id,max) ->
-          Some (id,Manual,(max,true))
+          Some (ExplByName id,Manual,(max,true))
        | (Anonymous,_), Some (Anonymous,max) ->
-          let id = Id.of_string ("arg_" ^ string_of_int k) in
-          Some (id,Manual,(max,true))
+          Some (ExplByPos (k,None),Manual,(max,true))
        | (Anonymous,_), None -> None
        end :: imps'
     | [], [] -> []
@@ -464,7 +467,7 @@ let implicits_of_global ref =
         | [], _ -> []
         | _, [] -> implicits
         | Some (_, x,y) :: implicits, Name id :: names ->
-           Some (id, x,y) :: rename implicits names
+           Some (ExplByName id, x,y) :: rename implicits names
         | imp :: implicits, _ :: names -> imp :: rename implicits names
       in
       List.map (fun (t, il) -> t, rename il rename_l) l
@@ -494,7 +497,7 @@ let impls_of_context ctx =
   let map decl =
     let id = NamedDecl.get_id decl in
     match Id.Map.get id !sec_implicits with
-    | Glob_term.Implicit -> Some (id, Manual, (true, true))
+    | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
     | Glob_term.Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -655,12 +658,12 @@ let compute_implicit_statuses autoimps l =
   let rec aux i = function
     | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
     | Name id :: autoimps, MaximallyImplicit :: manualimps ->
-       Some (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+       Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
     | Name id :: autoimps, Implicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
        let max = set_maximality imps' false in
        if max then warn_set_maximal_deprecated i;
-       Some (id, Manual, (max, true)) :: imps'
+       Some (ExplByName id, Manual, (max, true)) :: imps'
     | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
        user_err ~hdr:"set_implicits"
          (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))