diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 89ba78697c..abf5e6c2c0 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -89,7 +89,7 @@ val check_cofix : env -> cofixpoint -> unit parameter instantiation. This is used by the Ocaml extraction, which cannot handle (yet?) Prop-polymorphism. *) -exception SingletonInductiveBecomesProp of identifier +exception SingletonInductiveBecomesProp of Id.t val type_of_inductive_knowing_parameters : ?polyprop:bool -> env -> one_inductive_body -> types array -> types |