From 58153a5bc59bbde6534425d66a2fe5d9943eb44b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 15 Jan 2015 18:44:59 +0530
Subject: Minor fixes to the refman credits to be continued.

---
 doc/refman/RefMan-pre.tex | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 46ee361e09..e75ade9419 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -952,8 +952,7 @@ projects:
 
 The full integration of the proof engine brings to primitive tactics and
 the user level Ltac language deep tactic backtracking and multi-goal
-handling. This allows 
-...
+handling.
 
 The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
@@ -1014,13 +1013,12 @@ the relations between homotopy theory and type theory.
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-High-Level Specification Language:
-- tactics in terms
-- Universe inconsistency and unification error messages
-- Named existentials
-
-Opam Coq Guillaume Claret and Thomas Braibant 
+% High-Level Specification Language: 
+% - tactics in terms
+% - Universe inconsistency and unification error messages
+% - Named existentials
 
+% Opam Coq Guillaume Claret and Thomas Braibant 
 
 Maxime Dénès and Benjamin Grégoire developed an implementation of the
 conversion test using the OCaml native compiler.
-- 
cgit v1.2.3