From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 pretyping/inductiveops.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 5a4257e175..c74bbfe98b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -38,6 +38,8 @@ val lift_inductive_family  : int -> inductive_family -> inductive_family
 val substnl_ind_family :
   constr list -> int -> inductive_family -> inductive_family
 
+val relevance_of_inductive_family : env -> inductive_family -> Sorts.relevance
+
 (** An inductive type with its parameters and real arguments *)
 type inductive_type = IndType of inductive_family * EConstr.constr list
 val make_ind_type : inductive_family * EConstr.constr list -> inductive_type
@@ -47,6 +49,8 @@ val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
 val lift_inductive_type  : int -> inductive_type -> inductive_type
 val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
 
+val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance
+
 val mkAppliedInd : inductive_type -> EConstr.constr
 val mis_is_recursive_subset : int list -> wf_paths -> bool
 val mis_is_recursive :
@@ -176,7 +180,7 @@ val type_case_branches_with_names :
   env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
 
 (** Annotation for cases *)
-val make_case_info : env -> inductive -> case_style -> case_info
+val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info
 
 (** Make a case or substitute projections if the inductive type is a record
     with primitive projections.
-- 
cgit v1.2.3