diff options
| author | Maxime Dénès | 2014-04-10 20:05:26 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-10 20:08:11 -0400 |
| commit | 9f81e2c360c2be764e71d21ed7c266ee6e8a88c5 (patch) | |
| tree | 256503d5f8f21642f5759fc254fb672d4244eccc /kernel | |
| parent | 35f5a3fce53c8517d897660df6b66294d8662e46 (diff) | |
Fix guard condition for nested cofixpoints.
There were actually two problems, one of them being clearly unsound.
To make sure that this does not show up somewhere else in the code, it would
be better to resort to an abstraction keeping in sync the environment and the
De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index abc6ba4dfb..c0857566df 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -916,12 +916,12 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> - if (List.for_all (noccur_with_meta n nbfix) args) + if List.for_all (noccur_with_meta n nbfix) args then - let nbfix = Array.length vdefs in - if (Array.for_all (noccur_with_meta n nbfix) varit) then + if Array.for_all (noccur_with_meta n nbfix) varit then + let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) |