Fix bug #2262: bad implicit argument number by avoiding counting

products as implicit if they're part of a term and not a type (issue a
warning instead).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 46 insertions, 22 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ceb0748fee..1528589841 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1425,8 +1425,9 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
     | None -> ref Evd.empty
     | Some evdref -> evdref
   in
-  let c = intern_gen (kind=IsType) ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_rawterm c in
+  let istype = kind = IsType in
+  let c = intern_gen istype ~impls !evdref env c in
+  let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in
     Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 89ec5f1f11..cad48a5a1c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -295,19 +295,28 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    CAppExpl (loc, (None, id), args), avoid
 	in c, avoid
 
-let implicits_of_rawterm l =
+let implicits_of_rawterm ?(with_products=true) l =
   let rec aux i c =
-    match c with
-	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
-	  let rest = aux (succ i) b in
-	    if bk = Implicit then
-	      let name =
-		match na with
-		    Name id -> Some id
-		  | Anonymous -> None
-	      in
-		(ExplByPos (i, name), (true, true, true)) :: rest
-	    else rest
+    let abs loc na bk t b =
+      let rest = aux (succ i) b in
+	if bk = Implicit then
+	  let name =
+	    match na with
+	    | Name id -> Some id
+	    | Anonymous -> None
+	  in
+	    (ExplByPos (i, name), (true, true, true)) :: rest
+	else rest
+    in
+      match c with
+      | RProd (loc, na, bk, t, b) ->
+	  if with_products then abs loc na bk t b
+	  else 
+	    (if bk = Implicit then
+	       msg_warning (str "Ignoring implicit status of product binder " ++ 
+			      pr_name na ++ str " and following binders");
+	     [])
+      | RLambda (loc, na, bk, t, b) -> abs loc na bk t b
       | RLetIn (loc, na, t, b) -> aux i b
       | _ -> []
   in aux 1 l
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ac610fe78d..0b2ac3e71c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 76229076ca..a59cb96652 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -84,8 +84,10 @@ let find_with_index x l =
 
 open Vernacexpr
 
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
+  Constrintern.intern_constr evd env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
+  Constrintern.intern_type evd env
 
 let env_with_binders env isevars l =
   let rec aux ((env, rels) as acc) = function
@@ -109,19 +111,20 @@ let env_with_binders env isevars l =
 
 let subtac_process env isevars id bl c tycon =
   let c = Topconstr.abstract_constr_expr c bl in
-  let tycon =
+  let tycon, imps =
     match tycon with
-	None -> empty_tycon
+	None -> empty_tycon, None
       | Some t ->
 	  let t = Topconstr.prod_constr_expr t bl in
 	  let t = coqintern_type !isevars env t in
+	  let imps = Implicit_quantifiers.implicits_of_rawterm t in
 	  let coqt, ttyp = interp env isevars t empty_tycon in
-	    mk_tycon coqt
+	    mk_tycon coqt, Some imps
   in
   let c = coqintern_constr !isevars env c in
-  let imps = Implicit_quantifiers.implicits_of_rawterm c in
+  let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in
   let coqc, ctyp = interp env isevars c tycon in
-  let evm = non_instanciated_map env isevars ( !isevars) in
+  let evm = non_instanciated_map env isevars !isevars in
   let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
     evm, coqc, ty, imps
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2262.v b/test-suite/bugs/closed/shouldsucceed/2262.v
new file mode 100644
index 0000000000..b61f18b837
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2262.v
@@ -0,0 +1,11 @@
+
+
+Generalizable Variables A.
+Class Test A := { test : A }.
+
+Lemma mylemma : forall `{Test A}, test = test.
+Admitted. (* works fine *)
+
+Definition mylemma' := forall `{Test A}, test = test.
+About mylemma'.
+