#*********************************************************************
#                 Core base (util & heap)
#*********************************************************************
touch .depend
coq_makefile util.v util_tactic.v presburgerZ.v heap.v > Makefile.base
make -f Makefile.base depend
make -f Makefile.base

#*********************************************************************
#                 Integers Modulo (needs to be updated)
#*********************************************************************
#touch .depend
#coq_makefile intz.v > Makefile.int2
#make -f Makefile.int2 depend
#make -f Makefile.int2

#*********************************************************************
#                 Machine integers
#*********************************************************************
touch .depend
coq_makefile listbit.v listbit_correct.v machine_int.v > Makefile.int1
make -f Makefile.int1 depend
make -f Makefile.int1

#*********************************************************************
#                 Machine integers (specialized version)
#*********************************************************************
touch .depend
coq_makefile machine_int_spec.v > Makefile.int1_spec
make -f Makefile.int1_spec depend
make -f Makefile.int1_spec

#*********************************************************************
#                 seplog for mips_while
#*********************************************************************
touch .depend
coq_makefile state.v mips.v mips_tactics.v mips_contrib.v > Makefile.mips_while
make -f Makefile.mips_while depend
make -f Makefile.mips_while

#*********************************************************************
#                 sum and ssum predicates
#*********************************************************************
touch .depend
coq_makefile sum.v ssum.v > Makefile.sum
make -f Makefile.sum depend
make -f Makefile.sum

#*********************************************************************
#                 mapstos
#*********************************************************************
touch .depend
coq_makefile mapstos.v > Makefile.mapstos
make -f Makefile.mapstos depend
make -f Makefile.mapstos

#*********************************************************************
#                multiadd, multisub, multimul
#*********************************************************************
touch .depend
coq_makefile multiadd.v multisub.v multimul.v > Makefile.examples
make -f Makefile.examples depend
make -f Makefile.examples

#*********************************************************************
#                 Montgomery (spec)
#*********************************************************************
touch .depend
coq_makefile mont.v > Makefile.mont
make -f Makefile.mont depend
make -f Makefile.mont

#*********************************************************************
#  Montgomery (verif) (uncomment to compile, be careful, it's heavy)
#*********************************************************************
touch .depend
coq_makefile mont_verif.v > Makefile.mont_verif
make -f Makefile.mont_verif depend
make -f Makefile.mont_verif

#*********************************************************************
#  converters unsigned/signed multi-precision integers
#*********************************************************************
touch .depend
coq_makefile ssum_converter.v > Makefile.ssum_converter
make -f Makefile.ssum_converter depend
make -f Makefile.ssum_converter

#*********************************************************************
#                 Topsy (needs to be updated)
#*********************************************************************
#touch .depend
#coq_makefile topsy.v  > Makefile.topsy
#make -f Makefile.topsy depend
#make -f Makefile.topsy

#*********************************************************************
#                 seplog for unstructured mips
#*********************************************************************
touch .depend
coq_makefile mips0.v > Makefile.mips_goto
make -f Makefile.mips_goto depend
make -f Makefile.mips_goto

#*********************************************************************
#                 Documentation
#*********************************************************************
coqdoc --html -g -s -l *.v