From 5b653d2bb4d9f7b4c6f1faf4b3c17d6400cadf48 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 09:44:24 +0100 Subject: Reference manual/Credits: populate the "various smaller-scale improvements" part. --- doc/refman/RefMan-pre.tex | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index cf6dae34c..e16002227 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1014,21 +1014,29 @@ 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 - Maxime Dénès and Benjamin Grégoire developed an implementation of the conversion test using the OCaml native compiler. Maxime Dénès maintained the bytecode-based reduction machine. +Pierre-Marie Pédrot has extended the syntax of terms to, +experimentally, allow holes in terms to be solved by a locally +specified tactic. + +Existential variables are referred to by identifiers rather than mere +numbers, thanks to Hugo Herbelin. + +Error messages for universe inconsistencies have been improved by +Matthieu Sozeau. Error messages for unification and type inference +failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and +Arnaud Spiwack. + Pierre Courtieu contributed new features for using {\Coq} through Proof General and for better interactive experience (bullets, Search etc). +A distribution channel for Coq packages using the Opam tool has been +developed by Thomas Braibant and Guillaume Claret. + \begin{flushright} Paris, January 2015\\ Hugo Herbelin \& Matthieu Sozeau\\ -- cgit v1.2.3