diff options
| author | msozeau | 2010-06-09 18:19:16 +0000 |
|---|---|---|
| committer | msozeau | 2010-06-09 18:19:16 +0000 |
| commit | 2cf5036431304d5a3e6393d5fd5827798ea98983 (patch) | |
| tree | 1ef0caa5a199d7f5dc3703504c7c54a1b07d6bc4 /plugins | |
| parent | 41e36fe75b0859480c523e40361b75a13afcfe69 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 17 |
1 files changed, 10 insertions, 7 deletions
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 |