diff options
| author | Matthieu Sozeau | 2016-07-26 13:50:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-26 13:50:57 +0200 |
| commit | 273b8725e28e109b33f044079a36515d42068a8d (patch) | |
| tree | 3013d6b66b9ff2febb71d40d9e7fff8838e58a03 | |
| parent | 55dd78e3b40efc1b8000a1107daddc68d94814e5 (diff) | |
| parent | b36fc3478dc893b05edd2884972622531105d43d (diff) | |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
| -rw-r--r-- | checker/inductive.ml | 6 | ||||
| -rw-r--r-- | kernel/inductive.ml | 6 |
2 files changed, 8 insertions, 4 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 diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7b2d927162..3c4c2796ee 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -990,6 +990,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 id -> begin let open Context.Named.Declaration in @@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (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 Int.equal decr 0 then |