Skip to content

Commit cebb936

Browse files
committed
rename source directory coq->rocq
Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>
1 parent 8f2aa73 commit cebb936

116 files changed

Lines changed: 5 additions & 5 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

Dockerfile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
1717

1818

1919
COPY --chown=rocq:rocq _RocqProject Makefile Makefile.rocq_modules ./formal_ml/
20-
COPY --chown=rocq:rocq coq ./formal_ml/coq
20+
COPY --chown=rocq:rocq rocq ./formal_ml/rocq
2121

2222
RUN ["/bin/bash", "--login", "-c", "set -x && cd formal_ml && \
2323
make && make doc"]

Makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
# Contains the list of all the Coq modules
1+
# Contains the list of all the Rocq modules
22
include Makefile.rocq_modules
33

4-
ROCQ_FILES = $(addprefix coq/,$(MODULES:%=%.v))
4+
ROCQ_FILES = $(addprefix rocq/,$(MODULES:%=%.v))
55

66
all: rocq
77

@@ -21,7 +21,7 @@ GLOB_FILES_FOR_DOC = $(MODULES:%=%.glob)
2121
doc: rocq
2222
mkdir -p documentation/html
2323
rm -f documentation/html/*.html
24-
cd coq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(ROCQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
24+
cd rocq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(ROCQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
2525

2626
clean: clean-rocq
2727
rm -rf documentation/html

_RocqProject

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
-R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"
1+
-R rocq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"

0 commit comments

Comments
 (0)