From 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 13 Nov 2012 22:38:16 +0000
Subject: More monomorphizations

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c53a0bcd90..a44afce2b9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -190,7 +190,7 @@ let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort
+      if not polyprop && not (is_type0m_univ ar.poly_level) && is_prop_sort s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       mkArity (List.rev ctx,s)
 
-- 
cgit v1.2.3