wip

src/coq_elpi_utils.ml

@@ -43,19 +43,11 @@ let err ?loc msg =
   let loc = Option.map to_coq_loc loc in
   CErrors.user_err ?loc msg
 
-(* The loc is not "Loc.mergeable" (file name differs)
-  hence we generate an error feedback on the right loc *)
-[%%if coq = "8.20"]
-let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,CErrors.iprint ei)))
-[%%else]
-let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,[],CErrors.iprint ei)))
-[%%endif]
-
 let pp_oloc = function
   | None -> Pp.mt ()
   | Some loc -> Pp.str @@ Format.asprintf "%a " API.Ast.Loc.pp loc
 
-(* If the error comes from another file Coq drops the precise loc
+(* If the error comes from another file (see Loc.mergeable) Coq drops the precise loc
    and reports it on the whole execution site. If so, we print the
    more precise loc as part of the error message. *)
 let patch_loc_source execution_loc error_loc =