From 2cf5036431304d5a3e6393d5fd5827798ea98983 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 9 Jun 2010 18:19:16 +0000
Subject: 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
---
 plugins/subtac/subtac_pretyping.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'plugins')

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
 
-- 
cgit v1.2.3