Skip to content

Commit

Permalink
Split boolp and classical_sets in a new analysis package
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 committed Mar 22, 2022
1 parent 940be81 commit 52c0fc1
Show file tree
Hide file tree
Showing 44 changed files with 1,915 additions and 1,943 deletions.
7 changes: 7 additions & 0 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,13 @@ jobs:
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-mathcomp-analysis.opam'
install: |
startGroup "Install dependencies"
opam pin add -n -y -k path coq-mathcomp-classical $WORKDIR
opam pin add -n -y -k path $PACKAGE $WORKDIR
opam update -y
opam install -y -j 2 coq-mathcomp-classical.opam --deps-only
endGroup
custom_image: ${{ matrix.image }}

# See also:
Expand Down
35 changes: 18 additions & 17 deletions _CoqProject
Original file line number Diff line number Diff line change
@@ -1,44 +1,45 @@
-arg -w
-arg -parsing
-R classical mathcomp.classical
-R theories mathcomp.analysis

-arg -w -arg -parsing
-arg -w -arg +undeclared-scope
-arg -w -arg +non-primitive-record
-arg -w -arg +undeclared-scope
-arg -w -arg -ambiguous-paths
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant

theories/mathcomp_extra.v
theories/boolp.v
theories/ereal.v
theories/reals.v
classical/boolp.v
classical/classical_sets.v
classical/cardinality.v
classical/ereal.v
classical/forms.v
classical/fsbigop.v
classical/functions.v
classical/mathcomp_extra.v
classical/nsatz_realtype.v
classical/prodnormedzmodule.v
classical/reals.v
classical/Rstruct.v
classical/signed.v
classical/all_classical.v
theories/landau.v
theories/classical_sets.v
theories/Rstruct.v
theories/topology.v
theories/prodnormedzmodule.v
theories/normedtype.v
theories/realfun.v
theories/sequences.v
theories/exp.v
theories/trigo.v
theories/nsatz_realtype.v
theories/cardinality.v
theories/esum.v
theories/fsbigop.v
theories/set_interval.v
theories/lebesgue_measure.v
theories/forms.v
theories/derive.v
theories/measure.v
theories/numfun.v
theories/lebesgue_integral.v
theories/summability.v
theories/functions.v
theories/signed.v
theories/altreals/xfinmap.v
theories/altreals/discrete.v
theories/altreals/realseq.v
theories/altreals/realsum.v
theories/altreals/distr.v

-R theories mathcomp.analysis
23 changes: 23 additions & 0 deletions classical/Make
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
-R . mathcomp.classical

-arg -w -arg -parsing
-arg -w -arg +undeclared-scope
-arg -w -arg +non-primitive-record
-arg -w -arg -ambiguous-paths
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant

boolp.v
classical_sets.v
cardinality.v
ereal.v
forms.v
fsbigop.v
functions.v
mathcomp_extra.v
nsatz_realtype.v
prodnormedzmodule.v
reals.v
Rstruct.v
signed.v
all_classical.v
7 changes: 7 additions & 0 deletions classical/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# -*- Makefile -*-

# setting variables
COQPROJECT?=Make

# Main Makefile
include ../Makefile.common
Loading

0 comments on commit 52c0fc1

Please sign in to comment.