From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 28 Aug 2014 19:49:16 +0200
Subject: Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
---
 kernel/inductive.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index bac242f823..55236700d0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -53,6 +53,9 @@ val type_of_inductive_knowing_parameters :
 
 val elim_sorts : mind_specif -> sorts_family list
 
+val is_private : mind_specif -> bool
+val is_primitive_record : mind_specif -> bool
+
 (** Return type as quoted by the user *)
 
 val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
-- 
cgit v1.2.3