From 3cb4411089c18351d57685f9abe455d3f61f308f Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 2 Dec 2009 08:36:14 +0000
Subject: 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
---
 test-suite/check                |  25 --
 test-suite/parser/obj_magic.out | 609 ----------------------------------------
 test-suite/parser/obj_magic.v   |  22 --
 3 files changed, 656 deletions(-)
 delete mode 100644 test-suite/parser/obj_magic.out
 delete mode 100644 test-suite/parser/obj_magic.v

(limited to 'test-suite')

diff --git a/test-suite/check b/test-suite/check
index d0c5790bb..c5636a820 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -68,29 +68,6 @@ test_output() {
     done
 }
 
-# La fonction suivante teste l'analyseur syntaxique fournit par "coq-parser"
-# Elle fonctionne comme test_output
-test_parser() {
-    if [ -d $1 ]; then
-    for f in $1/*.v; do
-        nbtests=`expr $nbtests + 1`
-        printf "    "$f"..."
-        tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
-        foutput=`dirname $f`/`basename $f .v`.out
-        echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1
-        perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
-            $tmpoutput 2>&1 | grep -i error > /dev/null
-        if [ $? = 0 ] ; then
-            echo "Error! (unexpected output)"
-        else
-            echo "Ok"
-            nbtestsok=`expr $nbtestsok + 1`
-        fi
-        rm $tmpoutput
-    done
-    fi
-}
-
 # La fonction suivante teste en interactif 
 test_interactive() {
     for f in $1/*.v; do 
@@ -278,8 +255,6 @@ echo "Bugs tests"
 test_bugs bugs
 echo "Output tests"
 test_output output
-echo "Parser tests"
-test_parser parser
 echo "Interactive tests"
 test_interactive interactive
 echo "Micromega tests"
diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out
deleted file mode 100644
index 302fd6bb5..000000000
--- 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 7f0c23af6..000000000
--- 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.
-- 
cgit v1.2.3