diff options
| author | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
| commit | 633d9829d4e3678583c9e1ad161253fb53be1290 (patch) | |
| tree | 4c7edf5c090b369574b68d587787bac4b74d89ba /kernel/declarations.ml | |
| parent | adf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff) | |
| parent | 22b3b961804bea2c8b56cbab9a0c4902bf45c56c (diff) | |
Merge PR #11528: Checker does not rely on Monomorphic fields
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0b6e59bd5e..c550b0d432 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -32,6 +32,7 @@ type engagement = set_predicativity type template_arity = { template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; + template_context : Univ.ContextSet.t; } type ('a, 'b) declaration_arity = |