diff options
| author | Matthieu Sozeau | 2015-01-15 18:44:59 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | 93628d2e7156943edf3cfffa25a21855fb4b06db (patch) | |
| tree | 5addbf61623a35a72958786d126284f4af567051 | |
| parent | 47946681812adf60cc7ebdc9bdbcb7ade4a588a2 (diff) | |
Minor fixes to the refman credits to be continued.
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 14 |
1 files 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. |