aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 508ac0f65a..34de2f41bb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -430,9 +430,12 @@ type evar_flags =
restricted_evars : Evar.t Evar.Map.t;
typeclass_evars : Evar.Set.t }
+type side_effect_role =
+| Schema of inductive * string
+
type side_effects = {
seff_private : Safe_typing.private_constants;
- seff_roles : Entries.side_effect_role Cmap.t;
+ seff_roles : side_effect_role Cmap.t;
}
type evar_map = {