diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytecodes.ml | 3 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 8 |
2 files changed, 6 insertions, 5 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 940b5528d3..891d95378b 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -207,7 +207,8 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,_u) -> str "getglobal " ++ pr_con id + | Kgetglobal (id,u) -> + str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3c137ee92b..e3457006d0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -344,7 +344,7 @@ type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int | LocalNotConstructor - | LocalNonPar of int * int + | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -365,9 +365,9 @@ let explain_ind_err id ntyp env nbpar c nargs err = | LocalNotConstructor -> raise (InductiveError (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) - | LocalNonPar (n,l) -> + | LocalNonPar (n,i,l) -> raise (InductiveError - (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar)))) + (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) let failwith_non_pos n ntypes c = for k = n to n + ntypes - 1 do @@ -396,7 +396,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::hyps -> match kind_of_term (whd_betadeltaiota env lpar.(k)) with | Rel w when Int.equal w index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) + | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' |