Ajout g_xml.ml4 et cic2Xml.ml

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

1 files changed, 160 insertions, 0 deletions

diff --git a/.depend b/.depend
index bf87a7a5f4..418a36a934 100644
--- a/.depend
+++ b/.depend
@@ -3470,3 +3470,163 @@ tools/coqdoc/pretty.cmo: tools/coqdoc/output.cmi tools/coqdoc/index.cmi \
     tools/coqdoc/pretty.cmi 
 tools/coqdoc/pretty.cmx: tools/coqdoc/output.cmx tools/coqdoc/index.cmx \
     tools/coqdoc/pretty.cmi 
+tactics/tauto.cmo: parsing/grammar.cma
+tactics/tauto.cmx: parsing/grammar.cma
+tactics/eqdecide.cmo: parsing/grammar.cma
+tactics/eqdecide.cmx: parsing/grammar.cma
+tactics/extraargs.cmo: parsing/grammar.cma
+tactics/extraargs.cmx: parsing/grammar.cma
+tactics/extratactics.cmo: parsing/grammar.cma
+tactics/extratactics.cmx: parsing/grammar.cma
+tactics/eauto.cmo: parsing/grammar.cma
+tactics/eauto.cmx: parsing/grammar.cma
+contrib/omega/g_omega.cmo: parsing/grammar.cma
+contrib/omega/g_omega.cmx: parsing/grammar.cma
+contrib/romega/g_romega.cmo: parsing/grammar.cma
+contrib/romega/g_romega.cmx: parsing/grammar.cma
+contrib/ring/g_quote.cmo: parsing/grammar.cma
+contrib/ring/g_quote.cmx: parsing/grammar.cma
+contrib/ring/g_ring.cmo: parsing/grammar.cma
+contrib/ring/g_ring.cmx: parsing/grammar.cma
+contrib/field/field.cmo: parsing/grammar.cma
+contrib/field/field.cmx: parsing/grammar.cma
+contrib/fourier/g_fourier.cmo: parsing/grammar.cma
+contrib/fourier/g_fourier.cmx: parsing/grammar.cma
+contrib/extraction/g_extraction.cmo: parsing/grammar.cma
+contrib/extraction/g_extraction.cmx: parsing/grammar.cma
+contrib/xml/xmlentries.cmo: parsing/grammar.cma
+contrib/xml/xmlentries.cmx: parsing/grammar.cma
+contrib/jprover/jprover.cmo: parsing/grammar.cma
+contrib/jprover/jprover.cmx: parsing/grammar.cma
+contrib/cc/cctac.cmo: parsing/grammar.cma
+contrib/cc/cctac.cmx: parsing/grammar.cma
+contrib/funind/tacinv.cmo: parsing/grammar.cma
+contrib/funind/tacinv.cmx: parsing/grammar.cma
+contrib/first-order/g_ground.cmo: parsing/grammar.cma
+contrib/first-order/g_ground.cmx: parsing/grammar.cma
+contrib/interface/debug_tac.cmo: parsing/grammar.cma
+contrib/interface/debug_tac.cmx: parsing/grammar.cma
+contrib/interface/centaur.cmo: parsing/grammar.cma
+contrib/interface/centaur.cmx: parsing/grammar.cma
+parsing/lexer.cmo: 
+parsing/lexer.cmx: 
+parsing/q_util.cmo: 
+parsing/q_util.cmx: 
+parsing/q_coqast.cmo: 
+parsing/q_coqast.cmx: 
+parsing/g_prim.cmo: 
+parsing/g_prim.cmx: 
+parsing/pcoq.cmo: 
+parsing/pcoq.cmx: 
+parsing/g_basevernac.cmo: 
+parsing/g_basevernac.cmx: 
+parsing/g_minicoq.cmo: 
+parsing/g_minicoq.cmx: 
+parsing/g_vernac.cmo: 
+parsing/g_vernac.cmx: 
+parsing/g_proofs.cmo: 
+parsing/g_proofs.cmx: 
+parsing/g_cases.cmo: 
+parsing/g_cases.cmx: 
+parsing/g_xml.cmo: 
+parsing/g_xml.cmx: 
+parsing/g_constr.cmo: 
+parsing/g_constr.cmx: 
+parsing/g_module.cmo: 
+parsing/g_module.cmx: 
+parsing/g_tactic.cmo: 
+parsing/g_tactic.cmx: 
+parsing/g_ltac.cmo: 
+parsing/g_ltac.cmx: 
+parsing/argextend.cmo: 
+parsing/argextend.cmx: 
+parsing/tacextend.cmo: 
+parsing/tacextend.cmx: 
+parsing/vernacextend.cmo: 
+parsing/vernacextend.cmx: 
+parsing/g_primnew.cmo: 
+parsing/g_primnew.cmx: 
+parsing/g_vernacnew.cmo: 
+parsing/g_vernacnew.cmx: 
+parsing/g_proofsnew.cmo: 
+parsing/g_proofsnew.cmx: 
+parsing/g_constrnew.cmo: 
+parsing/g_constrnew.cmx: 
+parsing/g_tacticnew.cmo: 
+parsing/g_tacticnew.cmx: 
+parsing/g_ltacnew.cmo: 
+parsing/g_ltacnew.cmx: 
+toplevel/mltop.cmo: 
+toplevel/mltop.cmx: 
+lib/pp.cmo: 
+lib/pp.cmx: 
+lib/compat.cmo: 
+lib/compat.cmx: 
+contrib/xml/xml.cmo: 
+contrib/xml/xml.cmx: 
+contrib/xml/acic2Xml.cmo: 
+contrib/xml/acic2Xml.cmx: 
+contrib/xml/proofTree2Xml.cmo: 
+contrib/xml/proofTree2Xml.cmx: 
+contrib/interface/line_parser.cmo: 
+contrib/interface/line_parser.cmx: 
+tools/coq_makefile.cmo: 
+tools/coq_makefile.cmx: 
+tools/coq-tex.cmo: 
+tools/coq-tex.cmx: 
+coq_fix_code.o: kernel/byterun/coq_fix_code.c \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
+coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h
+coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h
+coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
+coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h
+coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h