aboutsummaryrefslogtreecommitdiff
path: root/test-suite/parser/obj_magic.out
diff options
context:
space:
mode:
authorglondu2009-12-02 08:36:14 +0000
committerglondu2009-12-02 08:36:14 +0000
commit3cb4411089c18351d57685f9abe455d3f61f308f (patch)
treec23e0d757eee079722f4fcc92b37e69c4ff4ef81 /test-suite/parser/obj_magic.out
parent3e253de6854b139a8a1be76af2388ffa9a3dcdb2 (diff)
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
Diffstat (limited to 'test-suite/parser/obj_magic.out')
-rw-r--r--test-suite/parser/obj_magic.out609
1 files changed, 0 insertions, 609 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