diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-07-25 16:39:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-07-25 16:40:58 +0200 |
| commit | ba00867d515624aee734d998bfbe3880f559d907 (patch) | |
| tree | a63e6cd8e7e65244eb1ed1a724967874914e17b1 | |
| parent | e10c9eed42e9cfc843a6cb2d48fa175c1be98741 (diff) | |
Fix bug #4876: critical bug in guard condition checker.
| -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 909ecccae..5825d1ab8 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -988,6 +988,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 = []) @@ -997,8 +1001,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 fbe0920bc..52f578987 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1010,6 +1010,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 match pi2 (lookup_named id renv.env) with @@ -1028,8 +1032,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 |