From 9e7e259e9f81eefd505b04e5e17b06136055e1ee Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Wed, 21 Jan 2015 09:07:10 +0100
Subject: Reference Manual/Credits: remove a duplicate.

---
 doc/refman/RefMan-pre.tex | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-pre.tex')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 4af5c8fc6..cf6dae34c 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1023,9 +1023,7 @@ and improvements regarding the different components of the system.
 
 Maxime Dénès and Benjamin Grégoire developed an implementation of the
 conversion test using the OCaml native compiler.
-Bruno Barras and Maxime Dénès fixed a problem in the guard condition
-leading to a refutation of standard axioms like propositional
-extensionality or univalence.
+
 Maxime Dénès maintained the bytecode-based reduction machine.
 
 Pierre Courtieu contributed new features for using {\Coq} through Proof
-- 
cgit v1.2.3

