Remove interface plugin

It has moved to the contribs (Sophia-Antipolis/Interface).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 631 deletions

diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out
deleted file mode 100644
index 302fd6bb50..0000000000
--- a/test-suite/parser/obj_magic.out
+++ /dev/null
@@ -1,609 +0,0 @@
-Starting Centaur Specialized Parser Loop
-message
-parsed
-1
-a
-vernac$int
-1
-n
-vernac$inv_regular
-0
-a
-vernac$ident
-H
-n
-vernac$none
-0
-n
-vernac$id_list
-0
-n
-vernac$inversion
-4
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$string
-exists _ : _ , _
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-a
-vernac$ident
-c
-n
-vernac$formula_list
-3
-n
-vernac$notation
-2
-n
-vernac$absurd
-1
-n
-vernac$try
-1
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-n
-vernac$discriminate_eq
-1
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-n
-vernac$simplify_eq
-1
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-n
-vernac$injection_eq
-1
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$hyp_location_list
-0
-n
-vernac$star
-0
-n
-vernac$clause
-2
-n
-vernac$none
-0
-n
-vernac$replace_with
-4
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$binding
-2
-n
-vernac$binding_list
-1
-n
-vernac$hyp_location_list
-0
-n
-vernac$star
-0
-n
-vernac$clause
-2
-n
-vernac$rewrite_rl
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$binding
-2
-n
-vernac$binding_list
-1
-a
-vernac$ident
-H1
-n
-vernac$hyp_location_list
-1
-n
-vernac$none
-0
-n
-vernac$clause
-2
-n
-vernac$rewrite_rl
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$int
-1
-a
-vernac$ident
-b
-n
-vernac$binding
-2
-n
-vernac$binding_list
-1
-n
-vernac$hyp_location_list
-0
-n
-vernac$star
-0
-n
-vernac$clause
-2
-n
-vernac$rewrite_lr
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$int
-1
-a
-vernac$ident
-b
-n
-vernac$binding
-2
-n
-vernac$binding_list
-1
-a
-vernac$ident
-H2
-n
-vernac$hyp_location_list
-1
-n
-vernac$none
-0
-n
-vernac$clause
-2
-n
-vernac$rewrite_lr
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-n
-vernac$deprewrite_lr
-1
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$string
-_ = _
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$formula_list
-2
-n
-vernac$notation
-2
-n
-vernac$none
-0
-n
-vernac$cutrewrite_lr
-2
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$string
-_ = _
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$formula_list
-2
-n
-vernac$notation
-2
-a
-vernac$ident
-H
-n
-vernac$cutrewrite_lr
-2
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$int
-3
-a
-vernac$int
-4
-a
-vernac$ident
-a
-n
-vernac$id_ne_list
-1
-n
-vernac$eauto_with
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-A
-a
-vernac$ident
-B
-a
-vernac$ident
-c
-n
-vernac$formula_ne_list
-1
-n
-vernac$appc
-2
-n
-vernac$formula_list
-2
-a
-vernac$int
-4
-n
-vernac$prolog
-2
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$int
-1
-a
-vernac$ident
-H2
-n
-vernac$binding
-2
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$binding
-2
-n
-vernac$binding_list
-2
-n
-vernac$eapply
-2
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$ident
-A
-a
-vernac$ident
-b
-n
-vernac$formula_ne_list
-1
-n
-vernac$appc
-2
-n
-vernac$id_list
-0
-n
-vernac$use_inversion
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-H
-a
-vernac$ident
-A
-a
-vernac$ident
-b
-n
-vernac$formula_ne_list
-1
-n
-vernac$appc
-2
-a
-vernac$ident
-H1
-a
-vernac$ident
-H2
-n
-vernac$id_list
-2
-n
-vernac$use_inversion
-3
-n
-vernac$none
-0
-n
-vernac$solve
-3
-a
-vernac$int
-1
-a
-vernac$ident
-ring
-a
-vernac$ident
-a
-a
-vernac$ident
-b
-n
-vernac$tactic_arg_list
-2
-n
-vernac$simple_user_tac
-2
-n
-vernac$none
-0
-n
-vernac$solve
-3
-n
-vernac$lr
-0
-a
-vernac$ident
-A
-a
-vernac$ident
-b
-n
-vernac$formula_ne_list
-1
-n
-vernac$appc
-2
-n
-vernac$formula_ne_list
-1
-a
-vernac$ident
-v
-n
-vernac$none
-0
-n
-vernac$idtac
-1
-n
-vernac$hintrewrite
-4
-n
-vernac$rl
-0
-a
-vernac$ident
-A
-a
-vernac$ident
-b
-n
-vernac$formula_ne_list
-1
-n
-vernac$appc
-2
-n
-vernac$formula_ne_list
-1
-a
-vernac$ident
-v
-n
-vernac$none
-0
-n
-vernac$auto
-1
-n
-vernac$hintrewrite
-4
-n
-vernac$command_list
-21
-e
-blabla
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
deleted file mode 100644
index 7f0c23af66..0000000000
--- a/test-suite/parser/obj_magic.v
+++ /dev/null
@@ -1,22 +0,0 @@
-inversion H.
-try absurd (exists a : b, c).
-discriminate H.
-simplify_eq H.
-injection H.
-replace a with b.
-rewrite <- H with (a := b).
-rewrite <- H with (a := b) in H1.
-rewrite H with (1 := b).
-rewrite H with (1 := b) in H2.
-dependent rewrite H.
-cutrewrite (a = b).
-cutrewrite (a = b) in H.
-eauto 3 4 with a.
-prolog [ A (B c) ] 4.
-eapply H with (1 := H2) (a := b).
-inversion H using (A b).
-inversion H using (A b) in H1 H2.
-ring a b.
-
-Hint Rewrite -> (A b) : v.
-Hint Rewrite <- (A b) using auto : v.