diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-07-15 16:19:01 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 00:47:37 +0200 |
| commit | b06d3badbf5a8aa95e5150c2dc0b3fd44e1269ab (patch) | |
| tree | 620cddfa84712137c61217e00429e5fae220ef45 /checker/indtypes.ml | |
| parent | 60b5e9c05e0c168e30eafede545c221e63d12ea2 (diff) | |
Implementing Herbelin's fix for the "NonPar" bug
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index e1a6bc7c1..f02f03dcb 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -269,7 +269,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 @@ -291,9 +291,9 @@ let explain_ind_err ntyp env0 nbpar c err = | LocalNotConstructor -> raise (InductiveError (NotConstructor (env,c',Rel (ntyp+nbpar)))) - | LocalNonPar (n,l) -> + | LocalNonPar (n,i,l) -> raise (InductiveError - (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) + (NonPar (env,c',n,Rel i,Rel (l+nbpar)))) let failwith_non_pos n ntypes c = for k = n to n + ntypes - 1 do @@ -323,7 +323,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when 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' |