From b1ec686f51c061d47535c408435a47e12a69ac5b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Dec 2017 18:58:24 +0100
Subject: 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.
---
 test-suite/success/abstract_poly.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
index b736b734fd..aa8da53361 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}.
-- 
cgit v1.2.3