diff options
| author | Maxime Dénès | 2018-09-12 17:12:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-12 17:12:20 +0200 |
| commit | 60103f4af881485c0f905ebcb6710b31744466d0 (patch) | |
| tree | 42c9f735a4904f7c97b8b47368c04c1a9eccc1c9 /kernel/inductive.ml | |
| parent | e3e1f56c38f345bccf984dd6d6d86fa06e423b96 (diff) | |
| parent | 55a328bb38f112cf2f456de4f1d9fc1bccaf88b1 (diff) | |
Merge PR #7109: Term combinators respecting the canonical structure of branches and return predicate
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4d13a5fcb8..1d2f22b006 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -932,7 +932,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest |