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/sigma.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/sigma.ml')

diff --git a/engine/sigma.ml b/engine/sigma.ml
index c7b0bb5a50..9381a33af1 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 =
-- 
cgit v1.2.3