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.

13 files changed, 34 insertions, 12 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0e6aaaa408..aa3fbc4577 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -398,7 +398,7 @@ let inh_app_fun_core ~program_mode env evd j =
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
-	let (evd',t) = Evardefine.define_evar_as_product evd ev in
+        let (evd',t) = Evardefine.define_evar_as_product env evd ev in
 	  (evd',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
       	try let t,p =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 99cd89cc2a..48e4b5414e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -597,6 +597,7 @@ let detype_universe sigma u =
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
+  | SProp -> GSProp
   | Prop -> GProp
   | Set -> GSet
   | Type u ->
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 55dfdc0574..799a81cf4b 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -72,7 +72,7 @@ let idx = Namegen.default_dependent_ident
 
 (* Refining an evar to a product *)
 
-let define_pure_evar_as_product evd evk =
+let define_pure_evar_as_product env evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
@@ -88,7 +88,7 @@ let define_pure_evar_as_product evd evk =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
     let src = subterm_source evk ~where:Codomain evksrc in
     let filter = Filter.extend 1 (evar_filter evi) in
-      if Sorts.is_prop (ESorts.kind evd1 s) then
+      if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar newenv evd1 concl ~src ~filter
       else
@@ -106,8 +106,8 @@ let define_pure_evar_as_product evd evk =
 
 (* Refine an applied evar to a product and returns its instantiation *)
 
-let define_evar_as_product evd (evk,args) =
-  let evd,prod = define_pure_evar_as_product evd evk in
+let define_evar_as_product env evd (evk,args) =
+  let evd,prod = define_pure_evar_as_product env evd evk in
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,rng = destProd evd prod in
   let evdom = mkEvar (fst (destEvar evd dom), args) in
@@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk =
   let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match EConstr.kind evd typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
-  | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
+  | Evar ev' -> let evd,typ = define_evar_as_product env evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
   let avoid = Environ.ids_of_named_context_val evi.evar_hyps in
   let id =
@@ -182,10 +182,10 @@ let split_tycon ?loc env evd tycon =
       match EConstr.kind evd t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev (* ev is undefined because of whd_all *) ->
-	    let (evd',prod) = define_evar_as_product evd ev in
+            let (evd',prod) = define_evar_as_product env evd ev in
 	    let (_,dom,rng) = destProd evd prod in
 	      evd',(Anonymous, dom, rng)
-	| App (c,args) when isEvar evd c ->
+        | App (c,args) when isEvar evd c ->
 	    let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in
 	    real_split evd' (mkApp (lam,args))
 	| _ -> error_not_product ?loc env evd c
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index cd23f9c601..7b5ced49bf 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -38,7 +38,7 @@ val split_tycon :
 val valcon_of_tycon : type_constraint -> val_constraint
 val lift_tycon : int -> type_constraint -> type_constraint
 
-val define_evar_as_product : evar_map -> existential -> evar_map * types
+val define_evar_as_product : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 8670c1d964..c57cf88cc6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -24,6 +24,7 @@ type existential_name = Id.t
 (** Sorts *)
 
 type 'a glob_sort_gen =
+  | GSProp (** representation of [SProp] literal *)
   | GProp (** representation of [Prop] literal *)
   | GSet  (** representation of [Set] literal *)
   | GType of 'a (** representation of [Type] literal *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bd321d5886..a9b419f03f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -588,6 +588,7 @@ let build_induction_scheme env sigma pind dep kind =
 (*s Eliminations. *)
 
 let elimination_suffix = function
+  | InSProp -> "_sind"
   | InProp -> "_ind"
   | InSet  -> "_rec"
   | InType -> "_rect"
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 6803ea7d9b..305ebf3dd5 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -153,6 +153,7 @@ let pattern_of_constr env sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
+    | Sort SProp -> PSort GSProp
     | Sort Prop -> PSort GProp
     | Sort Set -> PSort GSet
     | Sort (Type _) -> PSort (GType [])
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index dc6607557d..1a51ea4db7 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,6 +60,7 @@ type pretype_error =
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
     (Evar.t * Evar_kinds.t) option * Evar.Set.t option
+  | DisallowedSProp
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -171,6 +172,9 @@ let error_var_not_found ?loc env sigma s =
 let error_evar_not_found ?loc env sigma id =
   raise_pretype_error ?loc (env, sigma, EvarNotFound id)
 
+let error_disallowed_sprop env sigma  =
+  raise (PretypeError (env, sigma, DisallowedSProp))
+
 (*s Typeclass errors *)
 
 let unsatisfiable_constraints env evd ev comp =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index a0d459fe6b..82926ba280 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -67,6 +67,7 @@ type pretype_error =
   | UnsatisfiableConstraints of
     (Evar.t * Evar_kinds.t) option * Evar.Set.t option
     (** unresolvable evar, connex component *)
+  | DisallowedSProp
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -158,6 +159,8 @@ val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
 val error_evar_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
+val error_disallowed_sprop : env -> Evd.evar_map -> 'a
+
 (** {6 Typeclass errors } *)
 
 val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae1b4af3c3..62dd50d934 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -398,11 +398,13 @@ let pretype_id pretype k0 loc env sigma id =
 (* Main pretyping function                                               *)
 
 let interp_known_glob_level ?loc evd = function
+  | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
   | GType s -> interp_known_level_info ?loc evd s
 
 let interp_glob_level ?loc evd : glob_level -> _ = function
+  | GSProp -> evd, Univ.Level.sprop
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info ?loc evd s
@@ -452,6 +454,7 @@ let judge_of_Type ?loc evd s =
     evd, judge
 
 let pretype_sort ?loc sigma = function
+  | GSProp -> sigma, judge_of_sprop
   | GProp -> sigma, judge_of_prop
   | GSet -> sigma, judge_of_set
   | GType s -> judge_of_Type ?loc sigma s
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index fd3c77338c..1ca9e6590d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -150,7 +150,7 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop | Set -> Sorts.type1
+      | SProp | Prop | Set -> Sorts.type1
       | Type u -> Sorts.sort_of_univ (Univ.super u)
       end
     | Prod (name,t,c2) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ea6e52e1f8..ed020e243d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -65,7 +65,7 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
          match EConstr.kind sigma (whd_all env sigma typ) with
          | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in
              let (_,c1,c2) = destProd sigma t in
              sigma, (c1,c2)
          | _ ->
@@ -90,7 +90,7 @@ let judge_of_apply env sigma funj argjv =
          match EConstr.kind sigma (whd_all env sigma typ) with
          | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in
              let (_,c1,c2) = destProd sigma t in
              sigma, (c1,c2)
          | _ ->
@@ -230,6 +230,10 @@ let check_cofix env sigma pcofix =
 
 (* The typing machine with universes and existential variables. *)
 
+let judge_of_sprop =
+  { uj_val = EConstr.mkSProp;
+    uj_type = EConstr.type1 }
+
 let judge_of_prop =
   { uj_val = EConstr.mkProp;
     uj_type = EConstr.mkSort Sorts.type1 }
@@ -361,6 +365,9 @@ let rec execute env sigma cstr =
 
     | Sort s ->
       begin match ESorts.kind sigma s with
+        | SProp ->
+          if Environ.sprop_allowed env then sigma, judge_of_sprop
+          else error_disallowed_sprop env sigma
         | Prop -> sigma, judge_of_prop
         | Set -> sigma, judge_of_set
         | Type u -> sigma, judge_of_type u
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1ea16bbf34..9bd369a155 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -46,6 +46,7 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
 val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
   Names.Name.t array -> types array -> unsafe_judgment array -> evar_map
 
+val judge_of_sprop : unsafe_judgment
 val judge_of_prop : unsafe_judgment
 val judge_of_set : unsafe_judgment
 val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array ->