Turning "manual_implicits" into a list of position in impargs.ml.

1 files changed, 12 insertions, 12 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 01274e2568..ae1f55acda 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -30,16 +30,16 @@ let warn_implicits_in_term =
             strbrk "Discarding incompatible declaration in term.")
 
 let check_imps ~impsty ~impsbody =
-  let impsty = List.map (fun x -> x.CAst.v) impsty in
-  List.iter (fun {CAst.v = (key, (va:bool*bool*bool)); CAst.loc} ->
-      let b =
-        try
-          (* Pervasives.(=) is OK for this type *)
-          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va
-        with Not_found -> false
-      in
-      if not b then warn_implicits_in_term ?loc ())
-    impsbody
+  let rec aux impsty impsbody =
+  match impsty, impsbody with
+  | a1 :: impsty, a2 :: impsbody ->
+    (match a1.CAst.v, a2.CAst.v with
+    | None , None -> aux impsty impsbody
+    | Some _ , Some _ -> aux impsty impsbody
+    | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
+  | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+  | [], [] -> () in
+  aux impsty impsbody
 
 let interp_definition ~program_mode pl bl poly red_option c ctypopt =
   let env = Global.env() in
@@ -57,11 +57,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
     match tyopt with
     | None ->
       let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+      evd, c, imps1@impsbody, None
     | Some (ty, impsty) ->
       let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in
       check_imps ~impsty ~impsbody;
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+      evd, c, imps1@impsty, Some ty
   in
   (* Do the reduction *)
   let evd, c = red_constant_body red_option env_bl evd c in