File tree Expand file tree Collapse file tree 1 file changed +45
-0
lines changed Expand file tree Collapse file tree 1 file changed +45
-0
lines changed Original file line number Diff line number Diff line change
1
+ # -*- makefile-gmake -*-
2
+ M =.
3
+ P =Proof_of_Extensionality
4
+ COQ = time coqc
5
+ COQFLAGS = -opt -q
6
+ # in this list, put the prerequisites earlier, so TAGS is in the right order
7
+ VFILES := \
8
+ $M/Generalities/uuu.v \
9
+ $M/Generalities/uu0.v \
10
+ $P/funextfun.v \
11
+ $M/hlevel1/hProp.v \
12
+ $M/hlevel2/hSet.v \
13
+ $M/hlevel2/algebra1a.v \
14
+ $M/hlevel2/algebra1b.v \
15
+ $M/hlevel2/algebra1c.v \
16
+ $M/hlevel2/algebra1d.v \
17
+ $M/hlevel2/hnat.v \
18
+ $M/hlevel2/stnfsets.v \
19
+ $M/hlevel2/finitesets.v \
20
+ $M/hlevel2/hz.v \
21
+ $M/hlevel2/hq.v
22
+ VOFILES := $(VFILES:.v=.vo )
23
+ DOCFILES := doc/index.html
24
+ % .glob % .vo : % .v
25
+ @ echo " make: Entering directory \` $( dir $* ) '"
26
+ cd $(dir $* ) && $(COQ ) $(COQFLAGS ) $(notdir $* .v)
27
+ @ echo " make: Leaving directory \` $( dir $* ) '"
28
+ all : TAGS $(VOFILES ) $(DOCFILES )
29
+ COQDEFS := -r "/^[[:space:]]*\(Inductive\|Record\|Definition\|Corollary\|Axiom\|Theorem\|Notation\|Fixpoint\|Let\|Hypothesis\|Lemma\)[[:space:]]+['[:alnum:]_]+/"
30
+ TAGS : $(VFILES ) ; etags --language=none $(COQDEFS ) $^
31
+ Makefile.depends :; find . -name \* .v | >$@ xargs coqdep -I $M/Generalities -I $M/hlevel1 -I $M/hlevel2 -I $P
32
+ include Makefile.depends
33
+ MADE_FILES += doc
34
+ $(DOCFILES ) : $(VFILES ) ; mkdir -p doc && cd doc && ( find ../$M ../$P -name \* .v | xargs coqdoc -toc )
35
+ clean :
36
+ rm -rf $(MADE_FILES )
37
+ find $M $P \( \
38
+ -name \* .aux -o \
39
+ -name \* .dvi -o \
40
+ -name \* .idx -o \
41
+ -name \* .log -o \
42
+ -name \* .glob -o \
43
+ -name \* .vo -o \
44
+ -name \* .pdf \
45
+ \) -print -delete
You can’t perform that action at this time.
0 commit comments