diff options
| author | ppedrot | 2012-11-13 22:38:16 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-13 22:38:16 +0000 |
| commit | 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch) | |
| tree | e7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /kernel/inductive.ml | |
| parent | 1d436a18f2f72b57ea09a6d27709a36b63be863a (diff) | |
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |