diff options
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index e160022279..66f3369e3b 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1011,12 +1011,14 @@ taking into account the universe levels of indices when computing the levels of inductive types. This supports using Coq as a tool to explore the relations between homotopy theory and type theory. +Maxime Dénès and Benjamin Grégoire developed an implementation of +conversion test and normal form computation using the OCaml native +compiler. It complements the virtual machine conversion offering much +faster computation for expensive functions. + {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes and improvements regarding the different components of the system. -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, |