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.ml         | 3 ++-
 plugins/funind/indfun_common.ml  | 8 +++++++-
 plugins/funind/indfun_common.mli | 1 +
 3 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 42dc66dcf4..98d369aeda 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -49,7 +49,8 @@ let functional_induction with_clean c princl pat =
 		    user_err  (str "Cannot find induction information on "++
                                        Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 		in
-		match Tacticals.elimination_sort_of_goal g with
+                match Tacticals.elimination_sort_of_goal g with
+                | InSProp -> finfo.sprop_lemma
 		| InProp -> finfo.prop_lemma
 		| InSet -> finfo.rec_lemma
 		| InType -> finfo.rect_lemma
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cba3cc3d42..88546e9ae8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -199,6 +199,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; (* Has this function been defined using general recursive definition *)
     }
 
@@ -249,6 +250,7 @@ let subst_Function (subst,finfos) =
   let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
   let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
   let prop_lemma' =  Option.Smart.map do_subst_con finfos.prop_lemma in
+  let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
@@ -256,7 +258,8 @@ let subst_Function (subst,finfos) =
     completeness_lemma' == finfos.completeness_lemma &&
     rect_lemma' == finfos.rect_lemma &&
     rec_lemma' == finfos.rec_lemma &&
-    prop_lemma' == finfos.prop_lemma
+    prop_lemma' == finfos.prop_lemma &&
+    sprop_lemma' == finfos.sprop_lemma
   then finfos
   else
     { function_constant = function_constant';
@@ -267,6 +270,7 @@ let subst_Function (subst,finfos) =
       rect_lemma = rect_lemma' ;
       rec_lemma = rec_lemma';
       prop_lemma = prop_lemma';
+      sprop_lemma = sprop_lemma';
       is_general = finfos.is_general
     }
 
@@ -333,6 +337,7 @@ let add_Function is_general f =
   and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+  and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
     with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
@@ -345,6 +350,7 @@ let add_Function is_general f =
       rect_lemma = rect_lemma;
       rec_lemma = rec_lemma;
       prop_lemma = prop_lemma;
+      sprop_lemma = sprop_lemma;
       graph_ind = graph_ind;
       is_general = is_general
 
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