From 5cb337a0862e06a5b103b00c43cf9777e3468923 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 3 Jan 2019 16:59:58 +0100
Subject: Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record
---
 kernel/indTyping.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 2598548f3f..ad51af66a2 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
     - environment with inductives + parameters in rel context
     - abstracted universes
     - checked variance info
+    - record entry (checked to be OK)
     - parameters
     - for each inductive,
       (arity * constructors) (with params)
@@ -26,6 +27,7 @@ open Declarations
 val typecheck_inductive : env -> mutual_inductive_entry ->
   env
   * universes * Univ.Variance.t array option
+  * Names.Id.t array option option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
-- 
cgit v1.2.3