summaryrefslogtreecommitdiff
path: root/kernel/inductive.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.mli')
-rw-r--r--kernel/inductive.mli15
1 files changed, 12 insertions, 3 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a2bd674f..0dac719c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductive.mli 13368 2010-08-03 13:22:49Z barras $ i*)
+(*i $Id: inductive.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
@@ -85,7 +85,16 @@ val check_cofix : env -> cofixpoint -> unit
(*s Support for sort-polymorphic inductive types *)
-val type_of_inductive_knowing_parameters :
+(** The "polyprop" optional argument below allows to control
+ the "Prop-polymorphism". By default, it is allowed.
+ But when "polyprop=false", the following exception is raised
+ when a polymorphic singleton inductive type becomes Prop due to
+ parameter instantiation. This is used by the Ocaml extraction,
+ which cannot handle (yet?) Prop-polymorphism. *)
+
+exception SingletonInductiveBecomesProp of identifier
+
+val type_of_inductive_knowing_parameters : ?polyprop:bool ->
env -> one_inductive_body -> types array -> types
val max_inductive_sort : sorts array -> universe