From a1a3e3b84bc7dac2ae1ddae1770adde914732315 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 27 Apr 2012 16:43:24 +0000
Subject: Implicit arguments of Definition are taken from the type when given
 by the user.

There is a warning if the term is more precise.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/2733.v | 6 +++++-
 toplevel/command.ml                         | 6 +++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v
index 60c3719349..832de4f913 100644
--- a/test-suite/bugs/closed/shouldsucceed/2733.v
+++ b/test-suite/bugs/closed/shouldsucceed/2733.v
@@ -1,5 +1,8 @@
 Unset Asymmetric Patterns.
 
+Definition goodid : forall {A} (x: A), A := fun A x => x.
+Definition wrongid : forall A (x: A), A := fun {A} x => x.
+
 Inductive ty := N | B.
 
 Inductive alt_list : ty -> ty -> Type :=
@@ -21,4 +24,5 @@ alt_list t1 t3 :=
   | Bcons b l1 => fun _ l2 => Bcons b (app (@P) l1 l2)
   end.
 
-Check (fun {t t'} (l: alt_list t t') => app trullynul l nil).
+Check (fun {t t'} (l: alt_list t t') =>
+ app trullynul (goodid l) (wrongid _ nil)).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9deaa270f5..5aef9ec66d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -85,7 +85,11 @@ let interp_definition bl red_option c ctypopt =
 	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
-	imps1@(Impargs.lift_implicits nb_args imps2),
+	(* Check that all implicit arguments inferable from the term is inferable from the type *)
+	if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false)
+	then warn (str "Implicit arguments declaration relies on type." ++
+		     spc () ++ str "The term declares more implicits than the type here.");
+	imps1@(Impargs.lift_implicits nb_args impsty),
 	{ const_entry_body = body;
           const_entry_secctx = None;
 	  const_entry_type = Some typ;
-- 
cgit v1.2.3