From 968dfdb15cc11d48783017b2a91147b25c854ad6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Dec 2015 19:45:01 +0100
Subject: Monotonizing the Evarutil module.

Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
---
 engine/sigma.ml  | 12 ++++++++++++
 engine/sigma.mli |  7 +++++++
 2 files changed, 19 insertions(+)

(limited to 'engine')

diff --git a/engine/sigma.ml b/engine/sigma.ml
index e886b0d1e7..c25aac0c14 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,6 +36,18 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
+let new_univ_level_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_univ_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_sort_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
 let fresh_sort_in_family ?rigid env sigma s =
   let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
   Sigma (s, sigma, ())
diff --git a/engine/sigma.mli b/engine/sigma.mli
index cb948dba59..d7ae2e4ac9 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,6 +66,13 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Sorts.t, 'r) sigma
+
 val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
   'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
 val fresh_constant_instance :
-- 
cgit v1.2.3