diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-03 20:04:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-03 20:04:13 +0000 |
| commit | f1c2d541fb48f74f89e63a681d274de6b939a8db (patch) | |
| tree | df4a4b1cc1e2845a06f544f0f517ef54bf996bbe /toplevel | |
| parent | 321969d18e24a6c636137efd0a59a254603fce94 (diff) | |
Fixing bug using explictly declared implicit arguments in inductive arities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 3f4f15318..2e6fd8f49 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -239,7 +239,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in + let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in let arities = List.map fst arities in let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -273,7 +273,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = mind_entry_lc = ctypes }) indl arities constructors in let impls = - let len = List.length ctx_params in + let len = rel_context_nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors |