From cee131dea8805716da50468d99fdce2753e60e9e Mon Sep 17 00:00:00 2001
From: Yiyuan Cao <100843429+yiyuan-cao@users.noreply.github.com>
Date: Fri, 16 Feb 2024 07:08:22 +0800
Subject: [PATCH] Update README

fix: update the broken link to hollightcoq source archive
---
 Proofrecording/README | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Proofrecording/README b/Proofrecording/README
index f00b422c..92a52c32 100644
--- a/Proofrecording/README
+++ b/Proofrecording/README
@@ -4,7 +4,7 @@
 ****              EXPORTATION TO COQ             ****
 ****                                             ****
 ****          Steven Obua (obua@in.tum.de)       ****
-****         Technische Universität München      ****
+****         Technische Universität München      ****
 ****                February 2005                ****
 ****                     and                     ****
 **** Chantal Keller (keller@lix.polytechnique.fr)****
@@ -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.