diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 3a77a2b440..6345046431 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -483,6 +483,8 @@ let is_typeclass_evar evd evk = let flags = evd.evar_flags in Evar.Set.mem evk flags.typeclass_evars +let get_obligation_evars evd = evd.evar_flags.obligation_evars + let set_obligation_evar evd evk = let flags = evd.evar_flags in let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in @@ -889,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 *) (****************************************) |