diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-01-18 15:09:40 -0500 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-01-18 15:12:56 -0500 |
| commit | 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369 (patch) | |
| tree | 79575c89a4a0b26c9f8bf8bd9a5744edbd9e60f7 /checker/inductive.ml | |
| parent | 22bd27a46f6c91f2c74945333547e4657dcd1428 (diff) | |
Relaxing the sort elimination check to allow for let-bindings in arities.
I restored this in the kernel, and added it to the checker. There is one last
source of non-uniformity, which is the Sort case in the checker (was not
present in the kernel). I don't know what this case covers, so it should be
reviewed.
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index be0f220b2..c00a6c5dd 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -294,6 +294,8 @@ let is_correct_arity env c (p,pj) ind specif params = | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in |