From fcfa1e90df70b7fc00a4865fb48c1dc3250c58d9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 14 Aug 2014 14:14:25 +0200 Subject: Fix non-printing of coercions for primitive projections (fixes bug #3433). --- pretyping/inductiveops.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1561cf97b..03d41015b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -121,6 +121,10 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** Primitive projections *) +val projection_nparams : projection -> int +val projection_nparams_env : env -> projection -> int + (** Extract information from an inductive family *) type constructor_summary = { -- cgit v1.2.3