From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Oct 2017 14:03:51 +0200
Subject: Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
---
 plugins/funind/indfun_common.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1e0b95df34..102994f61e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -70,6 +70,7 @@ type function_info =
       rect_lemma : Constant.t option;
       rec_lemma : Constant.t option;
       prop_lemma : Constant.t option;
+      sprop_lemma : Constant.t option;
       is_general : bool;
     }
 
-- 
cgit v1.2.3


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.
---
 plugins/funind/indfun_common.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 102994f61e..4ec3131518 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -110,9 +110,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc
 val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
 
 val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
-  (Names.Name.t * EConstr.t) list * EConstr.t
-val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+  (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
+val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
+val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
 
 type tcc_lemma_value =
   | Undefined
-- 
cgit v1.2.3