From 9e7e259e9f81eefd505b04e5e17b06136055e1ee Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack 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