diff options
| author | Pierre-Marie Pédrot | 2019-09-26 15:36:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-26 15:54:24 +0200 |
| commit | acbf569a3b9f242fd704af9124c58697b8762d0d (patch) | |
| tree | f920fbebb00504f76c85678245de25946dac8d09 /kernel/type_errors.ml | |
| parent | 92006b6cc6b49ed6f892a7e5475f32ca852a9769 (diff) | |
Move the declararation of delayed constraints out of add_constant_aux.
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions