Skip to content

Commit

Permalink
Update README
Browse files Browse the repository at this point in the history
fix: update the broken link to hollightcoq source archive
  • Loading branch information
yiyuan-cao authored Feb 15, 2024
1 parent ea45176 commit cee131d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Proofrecording/README
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
**** EXPORTATION TO COQ ****
**** ****
**** Steven Obua ([email protected]) ****
**** Technische Universit�t M�nchen ****
**** Technische Universität München ****
**** February 2005 ****
**** and ****
**** Chantal Keller ([email protected])****
Expand Down Expand Up @@ -165,7 +165,7 @@ subdirectory $HOLPROOFEXPORTDIR/hollight/hollight.

4. To exploit the theorems that have been exported, you have to download
the Coq's interface at
<http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/hollightcoq-coq.tar.gz>.
<https://www.lri.fr/~keller/Documents-recherche/Stage09/hollightcoq-all.tar.gz>.
A README file explains how to use it.


Expand Down

0 comments on commit cee131d

Please sign in to comment.