diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c0f41d2bc9..48856c5c0d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1015,9 +1015,22 @@ 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 + | Proj (p, c) -> + begin try + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + with (FixGuardError _ as exn) -> + let exn = CErrors.push exn in + (* we try hard to reduce the proj away by looking for a + constructor in c (we unfold definitions too) *) + let c = whd_all renv.env c in + let hd, _ = decompose_app c in + match kind hd with + | Construct _ -> + check_rec_call renv [] + (Term.applist (mkProj(Projection.unfold p,c), l)) + | _ -> Exninfo.iraise exn + end | Var id -> begin |