diff options
| author | Guillaume Melquiond | 2016-08-10 11:26:30 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-10 11:26:30 +0200 |
| commit | 90303e38d22479105927f0dd2fe95cce9447bd44 (patch) | |
| tree | ab679c9f51a971c3b0f15b0b59108dbe36536fae /engine/sigma.mli | |
| parent | 8d4df809c90352035f7bc92e1f829f2d482625ed (diff) | |
Remove unused optional "predicative" argument.
Diffstat (limited to 'engine/sigma.mli')
| -rw-r--r-- | engine/sigma.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/sigma.mli b/engine/sigma.mli index aaf603efd8..7473a251b7 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -68,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_sort_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> |