From ba85529cc9df54a41b222c26a3328d361a1cda93 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 25 Nov 2010 16:16:27 +0000
Subject: Dp: minor fix suggested by Virgile Prevosto

 Non-dependent products in formulas were turned into implications,
 leading to some issues.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13656 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/dp/dp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/dp')

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 22ae4aaf9..00a76efa3 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -718,7 +718,7 @@ and tr_formula tv bv env f =
     | _, [a;b] when c = Lazy.force coq_iff ->
 	Iff (tr_formula tv bv env a, tr_formula tv bv env b)
     | Prod (n, a, b), _ ->
-	if is_imp_term f then
+        if is_Prop (Typing.type_of env Evd.empty a) then
 	  Imp (tr_formula tv bv env a, tr_formula tv bv env b)
 	else
 	  let id, t, bv, env, b = quantifiers n a b tv bv env in
-- 
cgit v1.2.3