diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/sigma.ml | 12 | ||||
| -rw-r--r-- | engine/sigma.mli | 7 |
2 files changed, 19 insertions, 0 deletions
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 : |