Remove unused optional "predicative" argument.

4 files changed, 16 insertions, 16 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 196f44760..e4b174bcb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -790,16 +790,16 @@ let merge_universe_subst evd subst =
 let with_context_set ?loc rigid d (a, ctx) =
   (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_level_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
-  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
+let new_sort_variable ?loc ?name rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name d in
     (d', Type u)
 
 let add_global_univ d u =
diff --git a/engine/evd.mli b/engine/evd.mli
index d6cf83525..942414511 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -508,9 +508,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 											   
diff --git a/engine/sigma.ml b/engine/sigma.ml
index c7b0bb5a5..9381a33af 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,16 +36,16 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
-let new_univ_level_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in
+let new_univ_level_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
-let new_univ_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in
+let new_univ_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
-let new_sort_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in
+let new_sort_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
 let fresh_sort_in_family ?loc ?rigid env sigma s =
diff --git a/engine/sigma.mli b/engine/sigma.mli
index aaf603efd..7473a251b 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -68,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_univ_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_sort_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
 
 val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->