diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-01 19:45:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 13:12:13 +0100 |
| commit | 968dfdb15cc11d48783017b2a91147b25c854ad6 (patch) | |
| tree | d619d1ebe51d29e5517c9c0385dc4aefe546edbe /engine | |
| parent | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (diff) | |
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.
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 e886b0d1e..c25aac0c1 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 cb948dba5..d7ae2e4ac 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 : |