diff options
| author | Matthieu Sozeau | 2015-01-15 18:44:59 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-15 18:59:00 +0530 |
| commit | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (patch) | |
| tree | 3e4ea3d379994a59d0e07f9a0dde760e5f636567 | |
| parent | 2d2b145ca9914df4b1eaab5acb3a11504b4308d5 (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. |