diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-20 18:58:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-11 11:17:34 +0100 |
| commit | b1ec686f51c061d47535c408435a47e12a69ac5b (patch) | |
| tree | 762134a4f927879ecd0ccb70226c683f575a7fe5 /kernel/term_typing.ml | |
| parent | 15bcba0cb00ef759169d2ef7c3cbc21b57f133d2 (diff) | |
Force polymorphic definitions to have no internal constraints.
The main contender was the abstract tactic that was generating useless
constraints for polymorphic subproofs that happened to contain themselves
monomorphic subproofs. We had to fix the test-suite for one particular
corner-case instance that looked more like a bug than anything else.
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions