From 90303e38d22479105927f0dd2fe95cce9447bd44 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 10 Aug 2016 11:26:30 +0200
Subject: Remove unused optional "predicative" argument.

---
 engine/evd.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index d6cf83525c..9424145113 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
 											   
-- 
cgit v1.2.3