From d4b3de96f524887013c0955bd5b90f0311f086e6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 11 Oct 2014 12:11:07 +0200
Subject: Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different
 name for the record binder of classes. This name is no longer generated in
 the kernel but part of the declaration. Also cleanup the interface to
 recognize primitive records based on an option type instead of a dynamic
 check of the length of an array.

---
 kernel/indtypes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0d5b034049..a231b6cf9d 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -41,7 +41,7 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive -> Id.t -> 
+val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.rel_context -> int array -> int array -> 
   Context.rel_context -> 
   (constant array * projection_body array)
-- 
cgit v1.2.3