diff options
author | 2006-06-16 14:41:51 +0000 | |
---|---|---|
committer | 2006-06-16 14:41:51 +0000 | |
commit | 35335c0605a84770f93965ea6b315cd369e9b731 (patch) | |
tree | 87b219b3275f8e21e88ed2970da3c056bc8f19e6 /library/impargs.ml | |
parent | fe730babfe0c01baa6c6da62460938f8839aa7c6 (diff) | |
parent | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff) |
Merge commit 'upstream/8.0pl3+8.1beta' into 8.1
Diffstat (limited to 'library/impargs.ml')
-rw-r--r-- | library/impargs.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 08ae2aa5..68fc046c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *) +(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Util open Names @@ -282,14 +282,15 @@ let compute_mib_implicits kn = let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity)) + (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)), + let ar = type_of_inductive (mib,mip) in + ((IndRef ind,auto_implicits env ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) - mip.mind_user_lc) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets |