diff options
| author | Julien Forest | 2017-06-16 16:45:47 +0200 |
|---|---|---|
| committer | Julien Forest | 2017-07-29 10:28:07 +0200 |
| commit | 3810a76a85a83242a739bacdfd2c8485a8e4c9da (patch) | |
| tree | f9c3b50a86f44c06e16aa74907e4050c5a609ecf /plugins/funind/functional_principles_proofs.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
closing bug 5315
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 |