]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/export_Paris_ZF/Makefile
All the equalityTactics have now been ported to use both the equality of
[helm.git] / 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