diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9ce9252073..82864bbe4c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -20,6 +20,9 @@ open Mod_subst (* This module defines the types of global declarations. This includes global constants/axioms and mutual inductive definitions *) +type engagement = ImpredicativeSet + + (*s Constants (internal representation) (Definition/Axiom) *) type constr_substituted = constr substituted @@ -191,3 +194,4 @@ and module_body = mod_type : module_type_body; mod_equiv : module_path option; mod_constraints : constraints } + |