Skip to content

Commit f3a155e

Browse files
mrhaandimrhaandi
committed
update opam and manual installation instructions
1 parent f87cc31 commit f3a155e

File tree

3 files changed

+69
-71
lines changed

3 files changed

+69
-71
lines changed

‎README.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88
```
99
opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
1010
eval $(opam env)
11-
opam pin add -k git rocq-runtime.dev "https://github.com/coq/coq.git#master"
12-
opam pin add -k git rocq-core.dev "https://github.com/coq/coq.git#master"
13-
opam pin add -k git rocq-stdlib.dev "https://github.com/coq/stdlib.git#master"
14-
opam pin add -k git rocq-prover.dev "https://github.com/coq/coq.git#master"
11+
opam install coq.9.0.0
12+
opam pin add -k git rocq-metarocq-utils.dev "https://github.com/MetaRocq/metarocq.git#9.0"
13+
opam pin add -k git rocq-metarocq-common.dev "https://github.com/MetaRocq/metarocq.git#9.0"
14+
opam pin add -k git rocq-metarocq-template.dev "https://github.com/MetaRocq/metarocq.git#9.0"
1515
```
1616

1717
# Coq Library of Undecidability Proofs

‎opam‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
opam-version: "2.0"
2-
version: "dev"
2+
version: "9.0"
33
maintainer: "[email protected]"
44
homepage: "https://github.com/uds-psl/coq-library-undecidability/"
55
dev-repo: "git+https://github.com/uds-psl/coq-library-undecidability/"
@@ -26,10 +26,8 @@ install: [
2626
[make "install"]
2727
]
2828
depends: [
29-
"rocq-core" {= "dev"}
30-
"rocq-stdlib" {= "dev"}
31-
"ocaml"
32-
# "coq-metacoq-template" {= "dev"}
29+
"coq" {= "9.0.0"}
30+
"coq-metacoq-template" {= "9.0"}
3331
]
3432

3533
synopsis: "A Coq Library of Undecidability Proofs"

‎theories/_CoqProject‎

Lines changed: 62 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -533,68 +533,68 @@ L/L_enum.v
533533

534534
#extraction framework
535535

536-
#L/Util/NaryApp.v
537-
#L/Util/ClosedLAdmissible.v
538-
539-
#L/Tactics/Computable.v
540-
#L/Tactics/LTactics.v
541-
#L/Tactics/Extract.v
542-
#L/Tactics/GenEncode.v
543-
#L/Tactics/Lbeta_nonrefl.v
544-
#L/Tactics/Lproc.v
545-
#L/Tactics/Lbeta.v
546-
#L/Tactics/Reflection.v
547-
#L/Tactics/LClos.v
548-
#L/Tactics/Lrewrite.v
549-
#L/Tactics/Lsimpl.v
550-
#L/Tactics/ComputableTactics.v
551-
552-
#L/Datatypes/LUnit.v
553-
#L/Datatypes/LBool.v
554-
#L/Datatypes/List/List_basics.v
555-
#L/Datatypes/List/List_enc.v
556-
#L/Datatypes/List/List_eqb.v
557-
#L/Datatypes/List/List_extra.v
558-
#L/Datatypes/List/List_in.v
559-
#L/Datatypes/List/List_nat.v
560-
#L/Datatypes/Lists.v
561-
#L/Datatypes/LNat.v
562-
#L/Datatypes/LOptions.v
563-
#L/Datatypes/LProd.v
564-
#L/Datatypes/LSum.v
565-
#L/Datatypes/LTerm.v
566-
#L/Datatypes/LFinType.v
567-
#L/Datatypes/LVector.v
568-
569-
#L/Functions/EqBool.v
570-
#L/Functions/Equality.v
571-
#L/Functions/Encoding.v
572-
#L/Functions/Proc.v
573-
#L/Functions/Subst.v
574-
#L/Functions/Eval.v
575-
#L/Functions/FinTypeLookup.v
576-
#L/Functions/Ackermann.v
577-
578-
#L/TM/TMEncoding.v
579-
#L/TM/TMinL.v
580-
#L/TM/TMinL/TMinL_extract.v
581-
#L/TM/TapeFuns.v
582-
#L/Reductions/TM_to_L.v
583-
#L/Reductions/H10_to_L.v
584-
#L/Reductions/PCPb_to_HaltL.v
585-
#L/Reductions/MuRec/MuRec_extract.v
586-
#L/Reductions/HaltMuRec_to_HaltL.v
587-
#L/Reductions/MuRec_computable_to_L_computable.v
588-
589-
#L/Computability/Acceptability.v
590-
#L/Computability/Computability.v
591-
#L/Computability/Decidability.v
592-
#L/Computability/Fixpoints.v
593-
#L/Computability/MuRec.v
594-
#L/Computability/Por.v
595-
#L/Computability/Synthetic.v
596-
#L/Computability/Scott.v
597-
#L/Computability/Rice.v
536+
L/Util/NaryApp.v
537+
L/Util/ClosedLAdmissible.v
538+
539+
L/Tactics/Computable.v
540+
L/Tactics/LTactics.v
541+
L/Tactics/Extract.v
542+
L/Tactics/GenEncode.v
543+
L/Tactics/Lbeta_nonrefl.v
544+
L/Tactics/Lproc.v
545+
L/Tactics/Lbeta.v
546+
L/Tactics/Reflection.v
547+
L/Tactics/LClos.v
548+
L/Tactics/Lrewrite.v
549+
L/Tactics/Lsimpl.v
550+
L/Tactics/ComputableTactics.v
551+
552+
L/Datatypes/LUnit.v
553+
L/Datatypes/LBool.v
554+
L/Datatypes/List/List_basics.v
555+
L/Datatypes/List/List_enc.v
556+
L/Datatypes/List/List_eqb.v
557+
L/Datatypes/List/List_extra.v
558+
L/Datatypes/List/List_in.v
559+
L/Datatypes/List/List_nat.v
560+
L/Datatypes/Lists.v
561+
L/Datatypes/LNat.v
562+
L/Datatypes/LOptions.v
563+
L/Datatypes/LProd.v
564+
L/Datatypes/LSum.v
565+
L/Datatypes/LTerm.v
566+
L/Datatypes/LFinType.v
567+
L/Datatypes/LVector.v
568+
569+
L/Functions/EqBool.v
570+
L/Functions/Equality.v
571+
L/Functions/Encoding.v
572+
L/Functions/Proc.v
573+
L/Functions/Subst.v
574+
L/Functions/Eval.v
575+
L/Functions/FinTypeLookup.v
576+
L/Functions/Ackermann.v
577+
578+
L/TM/TMEncoding.v
579+
L/TM/TMinL.v
580+
L/TM/TMinL/TMinL_extract.v
581+
L/TM/TapeFuns.v
582+
L/Reductions/TM_to_L.v
583+
L/Reductions/H10_to_L.v
584+
L/Reductions/PCPb_to_HaltL.v
585+
L/Reductions/MuRec/MuRec_extract.v
586+
L/Reductions/HaltMuRec_to_HaltL.v
587+
L/Reductions/MuRec_computable_to_L_computable.v
588+
589+
L/Computability/Acceptability.v
590+
L/Computability/Computability.v
591+
L/Computability/Decidability.v
592+
L/Computability/Fixpoints.v
593+
L/Computability/MuRec.v
594+
L/Computability/Por.v
595+
L/Computability/Synthetic.v
596+
L/Computability/Scott.v
597+
L/Computability/Rice.v
598598

599599
HOU/std/tactics.v
600600
HOU/std/misc.v

0 commit comments

Comments
 (0)