diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 15ab396e31..5f6d783598 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -821,8 +821,9 @@ let build_proof | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) + | Proj _ -> user_err Pp.(str "Prod") - | Prod _ -> user_err Pp.(str "Prod") + | Prod _ -> do_finalize dyn_infos g | LetIn _ -> let new_infos = { dyn_infos with |