OCAMLC config/coq_config.ml OCAMLC -o bin/coqmktop OCAMLOPT config/coq_config.ml OCAMLOPT lib/system.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLOPT library/library.ml OCAMLOPT library/states.ml OCAMLOPT -a -o library/library.cmxa OCAMLOPT pretyping/classops.ml OCAMLOPT pretyping/recordops.ml OCAMLOPT pretyping/evarconv.ml OCAMLOPT pretyping/coercion.ml OCAMLOPT pretyping/cases.ml OCAMLOPT pretyping/pretyping.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLOPT interp/symbols.ml OCAMLOPT interp/syntax_def.ml OCAMLOPT interp/constrintern.ml OCAMLOPT interp/modintern.ml OCAMLOPT interp/constrextern.ml OCAMLOPT interp/coqlib.ml OCAMLOPT library/declare.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT parsing/termast.ml OCAMLOPT parsing/esyntax.ml OCAMLOPT parsing/ppconstr.ml OCAMLOPT translate/ppconstrnew.ml OCAMLOPT parsing/printer.ml OCAMLOPT parsing/pptactic.ml OCAMLOPT translate/pptacticnew.ml OCAMLOPT parsing/prettyp.ml OCAMLOPT parsing/search.ml OCAMLOPT -a -o parsing/parsing.cmxa OCAMLOPT proofs/proof_trees.ml OCAMLOPT proofs/logic.ml OCAMLOPT proofs/refiner.ml OCAMLOPT proofs/evar_refiner.ml OCAMLOPT proofs/tacmach.ml OCAMLOPT proofs/clenv.ml OCAMLOPT proofs/pfedit.ml OCAMLOPT proofs/tactic_debug.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLOPT tactics/nbtermdn.ml OCAMLOPT tactics/tacticals.ml OCAMLOPT tactics/hipattern.ml OCAMLOPT tactics/tactics.ml OCAMLOPT tactics/hiddentac.ml OCAMLOPT tactics/elim.ml OCAMLOPT tactics/dhyp.ml OCAMLOPT tactics/auto.ml OCAMLOPT tactics/setoid_replace.ml OCAMLOPT tactics/equality.ml OCAMLOPT tactics/contradiction.ml OCAMLOPT tactics/inv.ml OCAMLOPT tactics/leminv.ml OCAMLOPT tactics/tacinterp.ml OCAMLOPT -a -o tactics/tactics.cmxa OCAMLOPT toplevel/himsg.ml OCAMLOPT toplevel/cerrors.ml OCAMLOPT toplevel/class.ml OCAMLOPT toplevel/metasyntax.ml OCAMLOPT toplevel/command.ml OCAMLOPT toplevel/record.ml OCAMLOPT toplevel/recordobj.ml OCAMLOPT toplevel/discharge.ml OCAMLOPT translate/ppvernacnew.ml OCAMLOPT toplevel/vernacinterp.ml OCAMLOPT toplevel/mltop.optml OCAMLOPT toplevel/vernacentries.ml OCAMLOPT toplevel/vernac.ml OCAMLOPT toplevel/protectedtoplevel.ml OCAMLOPT toplevel/toplevel.ml OCAMLOPT toplevel/usage.ml OCAMLOPT toplevel/coqinit.ml OCAMLOPT toplevel/coqtop.ml OCAMLOPT -a -o toplevel/toplevel.cmxa OCAMLOPT4 parsing/g_basevernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_vernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT parsing/g_natsyntax.ml OCAMLOPT parsing/g_zsyntax.ml OCAMLOPT parsing/g_rsyntax.ml OCAMLOPT -a -o parsing/highparsing.cmxa OCAMLOPT4 parsing/g_vernacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_proofsnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o parsing/highparsingnew.cmxa OCAMLOPT tactics/autorewrite.ml OCAMLOPT tactics/refine.ml OCAMLOPT4 tactics/extraargs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/extratactics.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/eauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/tauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/eqdecide.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o tactics/hightactics.cmxa OCAMLOPT contrib/omega/coq_omega.ml OCAMLOPT4 contrib/omega/g_omega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/romega/const_omega.ml OCAMLOPT contrib/romega/refl_omega.ml OCAMLOPT4 contrib/romega/g_romega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/ring/quote.ml OCAMLOPT4 contrib/ring/g_quote.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/ring/ring.ml OCAMLOPT4 contrib/ring/g_ring.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/field/field.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/fourier/fourierR.ml OCAMLOPT4 contrib/fourier/g_fourier.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/extraction/table.ml OCAMLOPT contrib/extraction/mlutil.ml OCAMLOPT contrib/extraction/modutil.ml OCAMLOPT contrib/extraction/ocaml.ml OCAMLOPT contrib/extraction/haskell.ml OCAMLOPT contrib/extraction/scheme.ml OCAMLOPT contrib/extraction/extraction.ml OCAMLOPT contrib/extraction/common.ml OCAMLOPT contrib/extraction/extract_env.ml OCAMLOPT4 contrib/extraction/g_extraction.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/jprover/jprover.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/xml/doubleTypeInference.ml OCAMLOPT contrib/xml/cic2acic.ml OCAMLOPT4 contrib/xml/acic2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/xml/proof2aproof.ml OCAMLOPT contrib/xml/xmlcommand.ml OCAMLOPT4 contrib/xml/proofTree2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/xml/xmlentries.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/cc/cctac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/funind/tacinvutils.ml OCAMLOPT4 contrib/funind/tacinv.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/first-order/formula.ml OCAMLOPT contrib/first-order/unify.ml OCAMLOPT contrib/first-order/sequent.ml OCAMLOPT contrib/first-order/rules.ml OCAMLOPT contrib/first-order/instances.ml OCAMLOPT contrib/first-order/ground.ml OCAMLOPT4 contrib/first-order/g_ground.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o contrib/contrib.cmxa COQMKTOP -o bin/coqtop.opt strip bin/coqtop.opt bin/coqtop.opt -boot -nois -compile theories/Init/Notations bin/coqtop.opt -boot -nois -compile theories/Init/Logic Defining 'IF' as keyword Defining 'exists2' as keyword bin/coqtop.opt -boot -nois -compile theories/Init/Datatypes bin/coqtop.opt -boot -nois -compile theories/Init/Peano bin/coqtop.opt -boot -nois -compile theories/Init/Specif bin/coqtop.opt -boot -nois -compile theories/Init/Logic_Type bin/coqtop.opt -boot -nois -compile theories/Init/Wf bin/coqtop.opt -boot -nois -compile theories/Init/Prelude bin/coqtop.opt -boot -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq bin/coqtop.opt -boot -compile theories/Logic/Hurkens bin/coqtop.opt -boot -compile theories/Logic/ProofIrrelevance bin/coqtop.opt -boot -compile theories/Logic/Classical_Prop bin/coqtop.opt -boot -compile theories/Logic/Classical_Pred_Type bin/coqtop.opt -boot -compile theories/Logic/Classical bin/coqtop.opt -boot -compile theories/Logic/Classical_Type bin/coqtop.opt -boot -compile theories/Logic/Classical_Pred_Set bin/coqtop.opt -boot -compile theories/Logic/Eqdep bin/coqtop.opt -boot -compile theories/Logic/ClassicalFacts bin/coqtop.opt -boot -compile theories/Logic/ChoiceFacts bin/coqtop.opt -boot -compile theories/Logic/Berardi bin/coqtop.opt -boot -compile theories/Logic/Eqdep_dec bin/coqtop.opt -boot -compile theories/Logic/Decidable bin/coqtop.opt -boot -compile theories/Logic/JMeq bin/coqtop.opt -boot -compile theories/Logic/ClassicalDescription bin/coqtop.opt -boot -compile theories/Logic/RelationalChoice bin/coqtop.opt -boot -compile theories/Logic/ClassicalChoice bin/coqtop.opt -boot -compile theories/Bool/Bool bin/coqtop.opt -boot -compile theories/Logic/Diaconescu bin/coqtop.opt -boot -compile theories/Arith/Le bin/coqtop.opt -boot -compile theories/Arith/Lt bin/coqtop.opt -boot -compile theories/Arith/Plus bin/coqtop.opt -boot -compile theories/Arith/Gt bin/coqtop.opt -boot -compile theories/Arith/Minus bin/coqtop.opt -boot -compile theories/Arith/Mult bin/coqtop.opt -boot -compile theories/Arith/Between bin/coqtop.opt -boot -compile theories/Arith/Peano_dec bin/coqtop.opt -boot -compile theories/Arith/Compare_dec bin/coqtop.opt -boot -compile theories/Arith/Factorial bin/coqtop.opt -boot -compile theories/Arith/Arith bin/coqtop.opt -boot -compile theories/Arith/Wf_nat bin/coqtop.opt -boot -compile theories/Arith/Min bin/coqtop.opt -boot -compile theories/Arith/Compare bin/coqtop.opt -boot -compile theories/Arith/Even bin/coqtop.opt -boot -compile theories/Arith/Div2 bin/coqtop.opt -boot -compile theories/Arith/EqNat bin/coqtop.opt -boot -compile theories/Arith/Euclid bin/coqtop.opt -boot -compile theories/Arith/Max bin/coqtop.opt -boot -compile theories/Bool/Sumbool bin/coqtop.opt -boot -compile theories/Arith/Bool_nat bin/coqtop.opt -boot -compile theories/Bool/IfProp bin/coqtop.opt -boot -compile theories/Bool/Zerob bin/coqtop.opt -boot -compile theories/Bool/DecBool bin/coqtop.opt -boot -compile theories/Bool/BoolEq bin/coqtop.opt -boot -compile theories/Bool/Bvector bin/coqtop.opt -boot -compile theories/NArith/BinPos bin/coqtop.opt -boot -compile theories/NArith/Pnat bin/coqtop.opt -boot -compile theories/NArith/BinNat bin/coqtop.opt -boot -compile theories/NArith/NArith bin/coqtop.opt -boot -compile theories/ZArith/BinInt bin/coqtop.opt -boot -compile theories/ZArith/Zcompare bin/coqtop.opt -boot -compile theories/ZArith/Zorder bin/coqtop.opt -boot -compile theories/ZArith/Znat bin/coqtop.opt -boot -compile theories/ZArith/Zmisc bin/coqtop.opt -boot -compile theories/ZArith/Wf_Z bin/coqtop.opt -boot -compile theories/ZArith/Zeven bin/coqtop.opt -boot -compile theories/ZArith/Zmin bin/coqtop.opt -boot -compile theories/ZArith/ZArith_dec bin/coqtop.opt -boot -compile theories/ZArith/Zabs bin/coqtop.opt -boot -compile theories/ZArith/auxiliary bin/coqtop.opt -boot -compile theories/ZArith/Zbool bin/coqtop.opt -boot -compile theories/ZArith/Zhints bin/coqtop.opt -boot -compile theories/ZArith/ZArith_base bin/coqtop.opt -boot -compile contrib/ring/Ring_theory bin/coqtop.opt -boot -compile contrib/ring/Quote bin/coqtop.opt -boot -compile contrib/ring/Ring_normalize bin/coqtop.opt -boot -compile contrib/ring/Ring_abstract bin/coqtop.opt -boot -compile contrib/ring/Ring bin/coqtop.opt -boot -compile contrib/ring/ArithRing bin/coqtop.opt -boot -compile contrib/ring/ZArithRing bin/coqtop.opt -boot -compile contrib/omega/OmegaLemmas bin/coqtop.opt -boot -compile contrib/omega/Omega bin/coqtop.opt -boot -compile theories/Lists/List bin/coqtop.opt -boot -compile theories/ZArith/Zcomplements bin/coqtop.opt -boot -compile theories/ZArith/Zsqrt bin/coqtop.opt -boot -compile theories/ZArith/Zpower bin/coqtop.opt -boot -compile theories/ZArith/Zdiv Defining 'mod' as keyword bin/coqtop.opt -boot -compile theories/ZArith/Zlogarithm bin/coqtop.opt -boot -compile theories/ZArith/ZArith bin/coqtop.opt -boot -compile theories/ZArith/Zwf bin/coqtop.opt -boot -compile theories/ZArith/Zbinary bin/coqtop.opt -boot -compile theories/ZArith/Znumtheory bin/coqtop.opt -boot -compile theories/Lists/MonoList bin/coqtop.opt -boot -compile theories/Lists/ListSet bin/coqtop.opt -boot -compile theories/Lists/Streams bin/coqtop.opt -boot -compile theories/Lists/TheoryList bin/coqtop.opt -boot -compile theories/Sets/Ensembles bin/coqtop.opt -boot -compile theories/Sets/Constructive_sets bin/coqtop.opt -boot -compile theories/Sets/Classical_sets bin/coqtop.opt -boot -compile theories/Sets/Permut bin/coqtop.opt -boot -compile theories/Sets/Relations_1 bin/coqtop.opt -boot -compile theories/Sets/Relations_1_facts bin/coqtop.opt -boot -compile theories/Sets/Partial_Order bin/coqtop.opt -boot -compile theories/Sets/Cpo bin/coqtop.opt -boot -compile theories/Sets/Powerset bin/coqtop.opt -boot -compile theories/Sets/Powerset_facts bin/coqtop.opt -boot -compile theories/Sets/Powerset_Classical_facts bin/coqtop.opt -boot -compile theories/Sets/Finite_sets bin/coqtop.opt -boot -compile theories/Sets/Finite_sets_facts bin/coqtop.opt -boot -compile theories/Sets/Image bin/coqtop.opt -boot -compile theories/Sets/Relations_2 bin/coqtop.opt -boot -compile theories/Sets/Infinite_sets bin/coqtop.opt -boot -compile theories/Sets/Relations_2_facts bin/coqtop.opt -boot -compile theories/Sets/Integers bin/coqtop.opt -boot -compile theories/Sets/Relations_3 bin/coqtop.opt -boot -compile theories/Sets/Multiset bin/coqtop.opt -boot -compile theories/Sets/Relations_3_facts bin/coqtop.opt -boot -compile theories/Sets/Uniset bin/coqtop.opt -boot -compile theories/IntMap/Addr bin/coqtop.opt -boot -compile theories/IntMap/Adist bin/coqtop.opt -boot -compile theories/IntMap/Addec bin/coqtop.opt -boot -compile theories/IntMap/Map bin/coqtop.opt -boot -compile theories/IntMap/Fset bin/coqtop.opt -boot -compile theories/IntMap/Adalloc bin/coqtop.opt -boot -compile theories/IntMap/Mapaxioms bin/coqtop.opt -boot -compile theories/IntMap/Mapiter bin/coqtop.opt -boot -compile theories/IntMap/Lsort bin/coqtop.opt -boot -compile theories/IntMap/Mapsubset bin/coqtop.opt -boot -compile theories/IntMap/Mapcard bin/coqtop.opt -boot -compile theories/IntMap/Mapcanon bin/coqtop.opt -boot -compile theories/IntMap/Mapc bin/coqtop.opt -boot -compile theories/IntMap/Mapfold bin/coqtop.opt -boot -compile theories/IntMap/Maplists bin/coqtop.opt -boot -compile theories/IntMap/Allmaps bin/coqtop.opt -boot -compile theories/Relations/Rstar bin/coqtop.opt -boot -compile theories/Relations/Newman bin/coqtop.opt -boot -compile theories/Relations/Relation_Definitions bin/coqtop.opt -boot -compile theories/Relations/Relation_Operators bin/coqtop.opt -boot -compile theories/Relations/Operators_Properties bin/coqtop.opt -boot -compile theories/Relations/Relations bin/coqtop.opt -boot -compile theories/Wellfounded/Disjoint_Union bin/coqtop.opt -boot -compile theories/Wellfounded/Inclusion bin/coqtop.opt -boot -compile theories/Wellfounded/Inverse_Image bin/coqtop.opt -boot -compile theories/Wellfounded/Transitive_Closure bin/coqtop.opt -boot -compile theories/Wellfounded/Lexicographic_Exponentiation bin/coqtop.opt -boot -compile theories/Wellfounded/Union bin/coqtop.opt -boot -compile theories/Wellfounded/Lexicographic_Product bin/coqtop.opt -boot -compile theories/Wellfounded/Well_Ordering bin/coqtop.opt -boot -compile theories/Wellfounded/Wellfounded bin/coqtop.opt -boot -compile theories/Reals/Rdefinitions bin/coqtop.opt -boot -compile theories/Reals/Raxioms bin/coqtop.opt -boot -compile contrib/field/Field_Compl bin/coqtop.opt -boot -compile contrib/field/Field_Theory bin/coqtop.opt -boot -compile contrib/field/Field_Tactic bin/coqtop.opt -boot -compile contrib/field/Field bin/coqtop.opt -boot -compile theories/Reals/RIneq bin/coqtop.opt -boot -compile theories/Reals/DiscrR bin/coqtop.opt -boot -compile theories/Reals/Rbase bin/coqtop.opt -boot -compile theories/Reals/R_Ifp bin/coqtop.opt -boot -compile contrib/fourier/Fourier_util bin/coqtop.opt -boot -compile contrib/fourier/Fourier bin/coqtop.opt -boot -compile theories/Reals/Rbasic_fun bin/coqtop.opt -boot -compile theories/Reals/R_sqr bin/coqtop.opt -boot -compile theories/Reals/SplitAbsolu bin/coqtop.opt -boot -compile theories/Reals/SplitRmult bin/coqtop.opt -boot -compile theories/Reals/ArithProp bin/coqtop.opt -boot -compile theories/Reals/Rfunctions bin/coqtop.opt -boot -compile theories/Reals/Rseries bin/coqtop.opt -boot -compile theories/Reals/SeqProp bin/coqtop.opt -boot -compile theories/Reals/Rcomplete bin/coqtop.opt -boot -compile theories/Reals/PartSum bin/coqtop.opt -boot -compile theories/Reals/AltSeries bin/coqtop.opt -boot -compile theories/Reals/Binomial bin/coqtop.opt -boot -compile theories/Reals/Rsigma bin/coqtop.opt -boot -compile theories/Reals/Rprod bin/coqtop.opt -boot -compile theories/Reals/Cauchy_prod bin/coqtop.opt -boot -compile theories/Reals/Alembert bin/coqtop.opt -boot -compile theories/Reals/SeqSeries bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_fun bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_def bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_alt bin/coqtop.opt -boot -compile theories/Reals/Cos_rel bin/coqtop.opt -boot -compile theories/Reals/Cos_plus bin/coqtop.opt -boot -compile theories/Reals/Rtrigo bin/coqtop.opt -boot -compile theories/Reals/Rlimit bin/coqtop.opt -boot -compile theories/Reals/Rderiv bin/coqtop.opt -boot -compile theories/Reals/RList bin/coqtop.opt -boot -compile theories/Reals/Ranalysis1 Defining 'o' as keyword bin/coqtop.opt -boot -compile theories/Reals/Ranalysis2 bin/coqtop.opt -boot -compile theories/Reals/Ranalysis3 bin/coqtop.opt -boot -compile theories/Reals/Rtopology bin/coqtop.opt -boot -compile theories/Reals/MVT bin/coqtop.opt -boot -compile theories/Reals/PSeries_reg bin/coqtop.opt -boot -compile theories/Reals/Exp_prop bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_reg bin/coqtop.opt -boot -compile theories/Reals/Rsqrt_def bin/coqtop.opt -boot -compile theories/Reals/R_sqrt bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_calc bin/coqtop.opt -boot -compile theories/Reals/Rgeom bin/coqtop.opt -boot -compile theories/Reals/Sqrt_reg bin/coqtop.opt -boot -compile theories/Reals/Ranalysis4 bin/coqtop.opt -boot -compile theories/Reals/Rpower bin/coqtop.opt -boot -compile theories/Reals/Ranalysis bin/coqtop.opt -boot -compile theories/Reals/NewtonInt bin/coqtop.opt -boot -compile theories/Reals/RiemannInt_SF bin/coqtop.opt -boot -compile theories/Reals/RiemannInt bin/coqtop.opt -boot -compile theories/Reals/Integration bin/coqtop.opt -boot -compile theories/Reals/Reals bin/coqtop.opt -boot -compile theories/Setoids/Setoid bin/coqtop.opt -boot -compile theories/Sorting/Permutation bin/coqtop.opt -boot -compile theories/Sorting/Sorting bin/coqtop.opt -boot -compile theories/Sorting/Heap bin/coqtop.opt -boot -compile contrib/romega/ReflOmegaCore Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable bin/coqtop.opt -boot -compile contrib/romega/ROmega bin/coqtop.opt -boot -compile contrib/ring/NArithRing bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring_theory bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring_normalize bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring bin/coqtop.opt -boot -compile contrib/cc/CCSolve OCAMLC -o bin/coqdep OCAMLC -o bin/coqdoc COQMKTOP -o bin/coqtop.byte OCAMLC -o bin/coqc bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Notations bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Logic bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Datatypes bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Peano bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Specif bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Logic_Type bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Wf bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Prelude bin/coqtop.opt -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states7/barestate.coq bin/coqtop.opt -boot -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Hurkens bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/ProofIrrelevance bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Classical_Prop bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Classical_Pred_Type bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Classical bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Classical_Type bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Classical_Pred_Set bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Eqdep bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/ClassicalFacts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/ChoiceFacts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Berardi bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Eqdep_dec Warning: Capture check in multiple binders not done Warning: Capture check in multiple binders not done bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Decidable bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/JMeq bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/ClassicalDescription bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/RelationalChoice bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/ClassicalChoice bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/Bool bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Logic/Diaconescu bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Le bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Lt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Plus bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Gt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Minus bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Mult bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Between bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Peano_dec bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Compare_dec bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Factorial bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Arith bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Wf_nat bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Min bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Compare bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Even bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Div2 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/EqNat bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Euclid bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Max bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/Sumbool bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Arith/Bool_nat bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/IfProp bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/Zerob bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/DecBool bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/BoolEq bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Bool/Bvector bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/NArith/BinPos Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition [fact:=(Prec positive xH [p,r:positive](times (add_un p) r))] [seven:=(xI (xI xH))] [five_thousand_forty:= (xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH))))))))))))] ((refl_equal positive (fact seven))::(fact seven)=five_thousand_forty) : (Prec positive xH [p,r:positive](times (add_un p) r) (xI (xI xH))) =(xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH)))))))))))) Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/NArith/Pnat bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/NArith/BinNat Translator warning: Unable to detect if H denotes a local definition bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/NArith/NArith bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/BinInt Translator warning: Unable to detect if H denotes a local definition bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zsyntax bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zcompare bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zorder Warning: Forgetting obsolete module Zsyntax Translator warning: Unable to detect if H denotes a local definition bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Znat bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zeven bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/ZArith_dec bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zbool bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zabs bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zmin bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zmisc bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Wf_Z bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/fast_integer bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/zarith_aux bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/auxiliary bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zhints bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/ZArith_base bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Ring_theory bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Quote bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Ring_normalize bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Ring_abstract Translator warning: Unable to detect if H0 denotes a local definition bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Ring bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/ArithRing bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/ZArithRing bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/omega/OmegaLemmas bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/omega/Omega bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/PolyList bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zcomplements bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zsqrt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zpower bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zdiv bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zlogarithm bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/ZArith bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zwf bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Zbinary bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/ZArith/Znumtheory bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/MonoList bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/ListSet bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/Streams bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/TheoryList bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/List bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Ensembles bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Constructive_sets bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Classical_sets bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Permut bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_1 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_1_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Partial_Order bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Cpo bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Powerset bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Powerset_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Powerset_Classical_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Finite_sets bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Finite_sets_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Image bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_2 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Infinite_sets bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_2_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Integers bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_3 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Multiset bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Relations_3_facts bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sets/Uniset bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Addr bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Adist bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Addec bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Map bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Fset bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Adalloc bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapaxioms bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapiter bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Lsort bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapsubset bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapcard bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapcanon bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapc bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Mapfold bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Maplists bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/IntMap/Allmaps bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Rstar bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Newman bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Relation_Definitions bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Lists/PolyListSyntax bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Relation_Operators bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Operators_Properties bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Relations/Relations bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Disjoint_Union bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Inclusion bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Inverse_Image bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Transitive_Closure bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Lexicographic_Exponentiation bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Union bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Lexicographic_Product bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Well_Ordering bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Wellfounded/Wellfounded bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rdefinitions bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rsyntax bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Raxioms bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/field/Field_Compl bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/field/Field_Theory bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/field/Field_Tactic bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/field/Field bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/RIneq bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/DiscrR bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rbase bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/R_Ifp bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/fourier/Fourier_util bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/fourier/Fourier bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rbasic_fun bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/R_sqr bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/SplitAbsolu bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/SplitRmult bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/ArithProp bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rfunctions bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rseries bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/SeqProp bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rcomplete bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/PartSum bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/AltSeries bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Binomial bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rsigma bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rprod bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Cauchy_prod bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Alembert bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/SeqSeries bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_fun bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_def bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_alt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Cos_rel bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Cos_plus bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rlimit bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rderiv bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/RList bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis1 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis2 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis3 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtopology bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/MVT bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/PSeries_reg bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Exp_prop bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_reg bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rsqrt_def bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/R_sqrt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_calc bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rgeom bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Sqrt_reg bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis4 bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Rpower bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/NewtonInt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/RiemannInt_SF bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/RiemannInt bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Integration bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Reals/Reals bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Setoids/Setoid bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sorting/Permutation bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sorting/Sorting bin/coqtop.opt -boot -translate -strict-implicit -compile theories7/Sorting/Heap bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ReflOmegaCore Warning: unable to ensure the correctness of the translation of an if-then-else Warning: unable to ensure the correctness of the translation of an if-then-else Warning: unable to ensure the correctness of the translation of an if-then-else Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ROmega bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/NArithRing bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_theory bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_normalize bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/cc/CCSolve bin/coqtop.opt -boot -compile ide/utf8 OCAMLC contrib/interface/ascent.mli OCAMLC contrib/interface/vtp.mli OCAMLC contrib/interface/vtp.ml OCAMLC contrib/interface/xlate.mli OCAMLC contrib/interface/xlate.ml OCAMLC contrib/interface/paths.mli OCAMLC contrib/interface/paths.ml OCAMLC contrib/interface/ctast.ml OCAMLC contrib/interface/translate.mli OCAMLC contrib/interface/translate.ml OCAMLC contrib/interface/pbp.mli OCAMLC contrib/interface/pbp.ml OCAMLC contrib/interface/dad.mli OCAMLC contrib/interface/dad.ml OCAMLC contrib/interface/history.mli OCAMLC contrib/interface/history.ml OCAMLC contrib/interface/name_to_ast.mli OCAMLC contrib/interface/name_to_ast.ml OCAMLC contrib/interface/debug_tac.mli OCAMLC4 contrib/interface/debug_tac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/interface/showproof_ct.ml OCAMLC contrib/interface/showproof.mli OCAMLC contrib/interface/showproof.ml OCAMLC contrib/interface/blast.mli OCAMLC contrib/interface/blast.ml OCAMLC4 contrib/interface/centaur.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. COQMKTOP -o bin/coq-interface OCAMLOPT contrib/interface/vtp.ml OCAMLOPT contrib/interface/xlate.ml OCAMLOPT contrib/interface/paths.ml OCAMLOPT contrib/interface/ctast.ml OCAMLOPT contrib/interface/translate.ml OCAMLOPT contrib/interface/pbp.ml OCAMLOPT contrib/interface/dad.ml OCAMLOPT contrib/interface/history.ml OCAMLOPT contrib/interface/name_to_ast.ml OCAMLOPT4 contrib/interface/debug_tac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/interface/showproof_ct.ml OCAMLOPT contrib/interface/showproof.ml OCAMLOPT contrib/interface/blast.ml OCAMLOPT4 contrib/interface/centaur.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. COQMKTOP -o bin/coq-interface.opt OCAMLC contrib/interface/line_parser.mli OCAMLC4 contrib/interface/line_parser.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/interface/parse.ml OCAMLC -o bin/parser OCAMLOPT4 contrib/interface/line_parser.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/interface/parse.ml OCAMLOPT -o bin/parser.opt