diff options
Diffstat (limited to 'doc')
| -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. |