aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2022-02-04 11:25:42 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2022-02-04 11:25:42 +0100
commit63544b2ce64071c9108573643f8bdd45df029165 (patch)
tree73eea878db27b7300931b793ddcec0383a702f3f
parent2c24be5412e9e223ab1eb964655477baa896ebee (diff)
downloadsmtcoq-63544b2ce64071c9108573643f8bdd45df029165.tar.gz
smtcoq-63544b2ce64071c9108573643f8bdd45df029165.zip
Temporarily switch to fork of trakt
-rw-r--r--coq-smtcoq.opam4
1 files changed, 2 insertions, 2 deletions
diff --git a/coq-smtcoq.opam b/coq-smtcoq.opam
index e597b1e..c50c7f2 100644
--- a/coq-smtcoq.opam
+++ b/coq-smtcoq.opam
@@ -16,7 +16,7 @@ depends: [
"coq-trakt"
]
pin-depends: [
- [ "coq-trakt.dev" "git+https://github.com/ecranceMERCE/trakt.git" ]
+ [ "coq-trakt.dev" "git+https://github.com/ckeller/trakt.git" ]
]
tags: [
"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
@@ -40,5 +40,5 @@ description: """
- a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
- decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination"""
url {
- src: "git+https://github.com/smtcoq/smtcoq.git#itp22"
+ src: "git+https://github.com/smtcoq/smtcoq.git#with-trakt"
}