diff options
| author | Hugo Herbelin | 2018-03-26 19:47:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-02 16:24:07 +0200 |
| commit | 8d46b60327e176391b470f38ce6d9f3a471c2959 (patch) | |
| tree | 7f25f371dd550bee0165f464a254d6a3711f6cc4 /kernel/inductive.ml | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Cosmetic: fixing an indentation
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 |