diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 13:57:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 13:57:13 +0200 |
| commit | a4ad14610cc0baab46264b179c4b8057f40d52c7 (patch) | |
| tree | 75782f47ebe381d84ea66409569167f9ba229c78 /test-suite/bugs/closed/3633.v | |
| parent | 9de1edd730eeb3cada742a27a36bc70178eda6d8 (diff) | |
Revert "While resolving typeclass evars in clenv, touch only the ones that appear in the"
This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8.
Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
Diffstat (limited to 'test-suite/bugs/closed/3633.v')
| -rw-r--r-- | test-suite/bugs/closed/3633.v | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v deleted file mode 100644 index 6f89ef6db..000000000 --- a/test-suite/bugs/closed/3633.v +++ /dev/null @@ -1,21 +0,0 @@ -Set Typeclasses Strict Resolution. -Class Contr (A : Type) := { center : A }. -Definition foo {A} `{Contr A} : A. -Proof. - apply center. - Undo. - (* Ensure the constraints are solved indepentently, otherwise a frozen ?A - makes a search for Contr ?A fail when finishing to apply (fun x => x) *) - apply (fun x => x), center. - -(* Toplevel input, characters 7-17: -Error: -Unable to satisfy the following constraints: -In environment: -A : Type -H : Contr A - -?A : "Type" -?Contr : "Contr ?X8" - - *)
\ No newline at end of file |