Merge PR #10134: Simplify impargs

Ack-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: jashug

1 files changed, 22 insertions, 38 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 90fb5a2036..806fe93297 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -497,9 +497,9 @@ type implicit_interactive_request =
 
 type implicit_discharge_request =
   | ImplLocal
-  | ImplConstant of Constant.t * implicits_flags
+  | ImplConstant of implicits_flags
   | ImplMutualInductive of MutInd.t * implicits_flags
-  | ImplInteractive of GlobRef.t * implicits_flags *
+  | ImplInteractive of implicits_flags *
       implicit_interactive_request
 
 let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits"
@@ -552,39 +552,24 @@ let add_section_impls vars extra_impls (cond,impls) =
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
-  | ImplInteractive (ref,flags,exp) ->
-    (try
-      let vars = variable_section_segment_of_reference ref in
-      let extra_impls = impls_of_context vars in
-      let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
-      Some (ImplInteractive (ref,flags,exp),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
-  | ImplConstant (con,flags) ->
-    (try
-      let vars = variable_section_segment_of_reference (ConstRef con) in
-      let extra_impls = impls_of_context vars in
-      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con,newimpls] in
-        Some (ImplConstant (con,flags),l')
-    with Not_found -> (* con not defined in this section *) Some (req,l))
-  | ImplMutualInductive (kn,flags) ->
-    (try
-      let l' = List.map (fun (gr, l) ->
-	let vars = variable_section_segment_of_reference gr in
-	let extra_impls = impls_of_context vars in
-        (gr,
-	 List.map (add_section_impls vars extra_impls) l)) l
-      in
-        Some (ImplMutualInductive (kn,flags),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
+  | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ ->
+     let l' =
+       try
+         List.map (fun (gr, l) ->
+             let vars = variable_section_segment_of_reference gr in
+             let extra_impls = impls_of_context vars in
+             let newimpls = List.map (add_section_impls vars extra_impls) l in
+             (gr, newimpls)) l
+       with Not_found -> l in
+     Some (req,l')
 
 let rebuild_implicits (req,l) =
   match req with
   | ImplLocal -> assert false
-  | ImplConstant (con,flags) ->
-      let oldimpls = snd (List.hd l) in
-      let newimpls = compute_constant_implicits flags con in
-      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
+  | ImplConstant flags ->
+      let ref,oldimpls = List.hd l in
+      let newimpls = compute_global_implicits flags ref in
+      req, [ref, List.map2 merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags kn in
       let rec aux olds news =
@@ -595,15 +580,14 @@ let rebuild_implicits (req,l) =
        | _, _ -> assert false
       in req, aux l newimpls
 
-  | ImplInteractive (ref,flags,o) ->
+  | ImplInteractive (flags,o) ->
+      let ref,oldimpls = List.hd l in
       (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
       | ImplAuto ->
-         let oldimpls = snd (List.hd l) in
          let newimpls = compute_global_implicits flags ref in
          [ref,List.map2 merge_impls oldimpls newimpls]
       | ImplManual userimplsize ->
-         let oldimpls = snd (List.hd l) in
          if flags.auto then
            let newimpls = List.hd (compute_global_implicits flags ref) in
            let p = List.length (snd newimpls) - userimplsize in
@@ -638,7 +622,7 @@ let declare_implicits_gen req flags ref =
 let declare_implicits local ref =
   let flags = { !implicit_args with auto = true } in
   let req =
-    if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
+    if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in
     declare_implicits_gen req flags ref
 
 let declare_var_implicits id =
@@ -647,7 +631,7 @@ let declare_var_implicits id =
 
 let declare_constant_implicits con =
   let flags = !implicit_args in
-    declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
+    declare_implicits_gen (ImplConstant flags) flags (ConstRef con)
 
 let declare_mib_implicits kn =
   let flags = !implicit_args in
@@ -697,7 +681,7 @@ let declare_manual_implicits local ref ?enriching l =
   let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
+    else ImplInteractive(flags,ImplManual (List.length autoimpls))
   in add_anonymous_leaf (inImplicits (req,[ref,l]))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
@@ -756,7 +740,7 @@ let set_implicits local ref l =
             compute_implicit_statuses autoimpls imps)) l in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
+    else ImplInteractive(flags,ImplManual (List.length autoimpls))
   in add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 let extract_impargs_data impls =