From f95017c2c69ee258ae570b789bce696357d2c365 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 May 2019 15:14:38 +0200
Subject: Adding location in warning telling implicit arguments differ in term
 and type.

---
 vernac/comFixpoint.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a31f3c34e0..1ded9f3d29 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -57,7 +57,7 @@ val interp_recursive :
   (* names / defs / types *)
   (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
-  (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
+  (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Exported for Funind *)
 
-- 
cgit v1.2.3