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.

3 files changed, 51 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/bug_3325.v b/test-suite/bugs/closed/bug_3325.v
index 36c065ebe8..835b8a7f33 100644
--- a/test-suite/bugs/closed/bug_3325.v
+++ b/test-suite/bugs/closed/bug_3325.v
@@ -1,13 +1,13 @@
 Typeclasses eauto := debug.
 Set Printing All.
 
-Axiom SProp : Set.
-Axiom sp : SProp.
+Axiom sProp : Set.
+Axiom sp : sProp.
 
 (* If we hardcode valueType := nat, it goes through *)
 Class StateIs := {
   valueType : Type;
-  stateIs : valueType -> SProp
+  stateIs : valueType -> sProp
 }.
 
 Instance NatStateIs : StateIs := {
@@ -17,17 +17,17 @@ Instance NatStateIs : StateIs := {
 Canonical Structure NatStateIs.
 
 Class LogicOps F := { land: F -> F }.
-Instance : LogicOps SProp. Admitted.
+Instance : LogicOps sProp. Admitted.
 Instance : LogicOps Prop. Admitted.
 
 Parameter (n : nat).
 (* If this is a [Definition], the resolution goes through fine. *)
 Notation vn := (@stateIs _ n).
 Definition vn' := (@stateIs _ n).
-Definition GOOD : SProp :=
+Definition GOOD : sProp :=
   @land _ _ vn'.
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
-Definition BAD : SProp :=
+Definition BAD : sProp :=
   @land _ _ vn.
 
 
diff --git a/test-suite/bugs/closed/bug_sprop_14.v b/test-suite/bugs/closed/bug_sprop_14.v
new file mode 100644
index 0000000000..1e6e9b30de
--- /dev/null
+++ b/test-suite/bugs/closed/bug_sprop_14.v
@@ -0,0 +1,26 @@
+(* -*- coq-prog-args: ("-allow-sprop"); -*- *)
+
+Set Universe Polymorphism.
+
+Inductive False : SProp :=.
+
+Axiom ℙ@{} : SProp.
+
+Definition TYPE@{i} := ℙ -> Type@{i}.
+Definition PROP@{} := ℙ -> SProp.
+
+Definition El@{i} (A : TYPE@{i}) := forall p, A p.
+Definition sEl@{} (A : PROP@{}) : SProp := forall p, A p.
+
+Definition SPropᶠ@{} := fun (p : ℙ) => SProp.
+
+Definition sProdᶠ@{i}
+  (A : TYPE@{i})
+  (B : forall (p : ℙ), El A -> SProp) : PROP := fun (p : ℙ) => forall x : El A, B p x.
+
+Definition Falseᶠ : El SPropᶠ := fun p => False.
+
+Definition EMᶠ : sEl (sProdᶠ SPropᶠ (fun p A => ((sProdᶠ A (fun p _ => Falseᶠ p))) p)).
+Proof.
+Fail Admitted.
+Abort.
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
new file mode 100644
index 0000000000..1e17d090c2
--- /dev/null
+++ b/test-suite/success/sprop.v
@@ -0,0 +1,19 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
+
+Check SProp.
+
+Definition iUnit : SProp := forall A : SProp, A -> A.
+Definition itt : iUnit := fun A a => a.
+
+Definition iSquash (A:Type) : SProp
+  := forall P : SProp, (A -> P) -> P.
+Definition isquash A : A -> iSquash A
+  := fun a P f => f a.
+
+Fail Check (fun A : SProp => A : Type).
+
+Lemma foo : Prop.
+Proof. pose (fun A : SProp => A : Type). Abort.
+
+(* define evar as product *)
+Check (fun (f:(_:SProp)) => f _).