Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box

 Nested was never constructed, while the notion of abstract_tactic_box
 is obsolete (cf. Refiner.abstract_tactic).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
Clean-up : no more Proof_type.proof_tree

 Btw, remove unused code in the xml plugin and in Tactic_printer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
Proof_type: rule now degenerates to prim_rule

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
Clean-up : removal of Proof_type.tactic_expr

 This instance of gen_tactic_expr was used only to decorate
 tactics via Refiner.abstract_tactics and alii, but these
 expressions are now ignored by the new proof-engine (no "info"...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
Tacexpr: revised version that doesn't need -rectypes

 For that, gen_atomic_tactic_expr and gen_tactic_expr are now
 mutually recursive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15866 85f007b7-540e-0410-9357-904b9bb8a0f7
avoid using rectypes in nametab.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15867 85f007b7-540e-0410-9357-904b9bb8a0f7
avoid using rectypes in dnet.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7
Adapt pieces of code needing -rectypes

 * in Matching and Tacinterp : ad-hoc types for encoding matching
   result and "next" continuation

 * in Class_tactics, occurrences of types such as
    "type t = (foo * (unit->t) option"
   have been specialized to something like
     type t = TNone | TSome of foo * (unit -> t)

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

 This file was providing the "Dump Tree" command to display
 the state of a proof in XML. This command has been broken since
 the integration of Arnaud's proof engine. Nobody cared enough
 to adapt this to the new framework, moreover the trend is
 rather now to use the xml-base dialog mode of coqtop,
 so I simply remove this obsolete code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15870 85f007b7-540e-0410-9357-904b9bb8a0f7
remove -rectypes except for term.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
remove Refiner.abstract_tactic and similar

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
cosmetic concerning interp of TacShowHyps

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15873 85f007b7-540e-0410-9357-904b9bb8a0f7
remove useless hidden_flag in TacMutual(Co)Fix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
no need for camlp4 cma's in coq misc tools

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 85f007b7-540e-0410-9357-904b9bb8a0f7
Minor fix in the ./build wrapper for ocamlbuild

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

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