diff options
| author | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
| commit | dc1db99e019242c07f00837f8316a8d392c40258 (patch) | |
| tree | ff271f3a63d9b4e7e6bf6bde4c590003c549c2c4 /checker | |
| parent | 139204928e55f92f02d3b3dd1d6746e34fdcdb88 (diff) | |
| parent | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (diff) | |
Merge branch 'v8.6' into trunk
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/inductive.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index cb344c7fd6..c4ffc141ff 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -989,6 +989,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -998,8 +1002,6 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - | Proj (p, c) -> check_rec_call renv [] c - and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body |