helm/EXPORT/export_Paris_ZF/Makefile

   1 all: objects theories
   2
   3 objects:
   4         coqc -R ZF/src Paris.ZF ZF/src/nothing.v
   5         coqc -R ZF/src Paris.ZF ZF/src/useful.v
   6         coqc -R ZF/src Paris.ZF ZF/src/ZFbasis.v
   7         coqc -R ZF/src Paris.ZF ZF/src/axs_extensionnalite.v
   8         coqc -R ZF/src Paris.ZF ZF/src/axs_paire.v
   9         coqc -R ZF/src Paris.ZF ZF/src/axs_reunion.v
  10         coqc -R ZF/src Paris.ZF ZF/src/axs_parties.v
  11         coqc -R ZF/src Paris.ZF ZF/src/axs_comprehension.v
  12         coqc -R ZF/src Paris.ZF ZF/src/axs_remplacement.v
  13         coqc -R ZF/src Paris.ZF ZF/src/couples.v
  14         coqc -R ZF/src Paris.ZF ZF/src/applications.v
  15         coqc -R ZF/src Paris.ZF ZF/src/axs_choice.v
  16         coqc -R ZF/src Paris.ZF ZF/src/axs_fundation.v
  17         coqc -R ZF/src Paris.ZF ZF/src/ZFrelations.v
  18         coqc -R ZF/src Paris.ZF ZF/src/MSetBasis.v
  19         echo "Load Verbose prova_Paris_ZF." | coqtop.byte -R ZF/src Paris.ZF
  20
  21 theories:
  22         ./exporttheories.sh
  23
  24 clean:
  25         rm -f *.vo ZF/src/*.vo