diff options
| -rw-r--r-- | engine/evd.ml | 3 | ||||
| -rw-r--r-- | engine/evd.mli | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | engine/uState.mli | 8 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_8908.v | 8 |
6 files changed, 27 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b3848e1b5b..6345046431 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -891,6 +891,9 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } +let make_nonalgebraic_variable evd u = + { evd with universes = UState.make_nonalgebraic_variable evd.universes u } + (****************************************) (* Operations on constants *) (****************************************) diff --git a/engine/evd.mli b/engine/evd.mli index be54bebcd7..0a8d1f3287 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -561,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map (** See [UState.make_flexible_variable] *) +val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map +(** See [UState.make_nonalgebraic_variable]. *) + val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/uState.ml b/engine/uState.ml index 41905feab7..dc760e7f97 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -577,6 +577,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_nonalgebraic_variable ctx u = + { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } + let make_flexible_nonalgebraic ctx = {ctx with uctx_univ_algebraic = Univ.LSet.empty} diff --git a/engine/uState.mli b/engine/uState.mli index 8053a7bf83..ad0cd5c1bb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t Turn the variable [l] flexible, and algebraic if [algebraic] is true and [l] can be. That is if there are no strict upper constraints on [l] and and it does not appear in the instance of any non-algebraic - universe. Otherwise the variable is just made flexible. *) + universe. Otherwise the variable is just made flexible. + + If [l] is already algebraic it will remain so even with [algebraic:false]. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +val make_nonalgebraic_variable : t -> Univ.Level.t -> t +(** Make the level non algebraic. Undefined behaviour on + already-defined algebraics. *) + (** Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations). *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96213af9c6..4692fe0057 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if not onlyalg then refresh_sort status ~direction s else t | UnivFlexible alg -> - if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) - else t)) + (if alg then + evdref := Evd.make_nonalgebraic_variable !evdref l); + t)) | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) diff --git a/test-suite/bugs/closed/bug_8908.v b/test-suite/bugs/closed/bug_8908.v new file mode 100644 index 0000000000..9c85839b75 --- /dev/null +++ b/test-suite/bugs/closed/bug_8908.v @@ -0,0 +1,8 @@ +Record foo : Type := + { fooA : Type; fooB : Type }. +Definition id {A : Type} (a : A) := a. +Definition untypable : Type. + unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y). + exact foo. + constructor. exact unit. exact unit. +Defined. |