File tree Expand file tree Collapse file tree 2 files changed +36
-0
lines changed Expand file tree Collapse file tree 2 files changed +36
-0
lines changed Original file line number Diff line number Diff line change 1+ opam-version: "2.0"
2+ maintainer: "erik@martin-dorel.org"
3+ version: "dev"
4+
5+ homepage: "https://github.com/erikmd/docker-coq-github-action-demo"
6+ dev-repo: "git+https://github.com/erikmd/docker-coq-github-action-demo.git"
7+ bug-reports: "https://github.com/erikmd/docker-coq-github-action-demo/issues"
8+ license: "MIT"
9+
10+ synopsis: "Demo of docker-coq-action"
11+ description: """
12+ Demo of docker-coq-action.
13+ """
14+
15+ build: [
16+ ["sh" "-c" "coq_makefile src/test.v -o Makefile2"]
17+ [make "-j%{jobs}%" "-f" "Makefile2"]
18+ ]
19+ install: [make "install" "-f" "Makefile2"]
20+
21+ depends: [
22+ "ocaml" {>= "4.05.0"}
23+ "coq" {(>= "8.6") | (= "dev")}
24+ ]
25+
26+ tags: [
27+ ]
28+ authors: [
29+ "Erik Martin-Dorel"
30+ ]
Original file line number Diff line number Diff line change 1+ Lemma id : forall A : Type, A -> A.
2+ Proof .
3+ exact (fun A (x : A) => x).
4+ Defined .
5+
6+ Print id.
You can’t perform that action at this time.
0 commit comments