diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:26:30 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:26:30 +0200 |
| commit | 90303e38d22479105927f0dd2fe95cce9447bd44 (patch) | |
| tree | ab679c9f51a971c3b0f15b0b59108dbe36536fae /engine/evd.ml | |
| parent | 8d4df809c90352035f7bc92e1f829f2d482625ed (diff) | |
Remove unused optional "predicative" argument.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 196f44760..e4b174bcb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -790,16 +790,16 @@ let merge_universe_subst evd subst = let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_level_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?loc ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in +let new_sort_variable ?loc ?name rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name d in (d', Type u) let add_global_univ d u = |