From 3810a76a85a83242a739bacdfd2c8485a8e4c9da Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Fri, 16 Jun 2017 16:45:47 +0200
Subject: closing bug 5315

---
 plugins/funind/functional_principles_proofs.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

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
-- 
cgit v1.2.3