diff options
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 |