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 /test-suite/success/abstract_poly.v | |
| 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 'test-suite/success/abstract_poly.v')
| -rw-r--r-- | test-suite/success/abstract_poly.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v index b736b734f..aa8da5336 100644 --- a/test-suite/success/abstract_poly.v +++ b/test-suite/success/abstract_poly.v @@ -17,4 +17,4 @@ intros m n P e p. abstract (rewrite e in p; exact p). Defined. -Check bar_subproof@{Set Set Set}. +Check bar_subproof@{Set Set}. |