1 files changed, 0 insertions, 19 deletions
diff --git a/test-suite/output/Implicit.v8 b/test-suite/output/Implicit.v8
deleted file mode 100644
index e18ae5513..000000000
--- a/test-suite/output/Implicit.v8
+++ /dev/null
@@ -1,19 +0,0 @@
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(* Suggested by Pierre Casteran (bug #169) *)
-(* Argument 3 is needed to typecheck and should be printed *)
-Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
-Check (compose (C:=nat) S).
-
-(* Better to explicitly display the arguments inferable from a
-   position that could disappear after reduction *)
-Inductive ex (A : Set) (P : A -> Prop) : Prop :=
-    ex_intro : forall x : A, P x -> ex P.
-Check (ex_intro (P:=fun _ => True) (x:=0) I).
-
-(* Test for V8 printing of implicit by names *)
-Definition d1 y x (h : x = y :>nat) := h.
-Definition d2 x := d1 (y:=x).
-
-Print d2.
-\ No newline at end of file