diff options
| author | Pierre Boutillier | 2014-09-03 15:18:27 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-09-03 15:18:27 +0200 |
| commit | 1e4a15e74114cef528e76f9aa8b0aeb78e82aecc (patch) | |
| tree | a093f1ac31d37e7b28c84c0617253b90db0e8dc2 /doc/refman/RefMan-pre.tex | |
| parent | d34cb7cc523fe7f6e9b371cee17b7f7b7e588ddf (diff) | |
sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 1e83bd956b..23d4ee10d8 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -201,7 +201,7 @@ Gérard Huet %\addcontentsline{toc}{section}{Credits: addendum for version V6.1} The present version 6.1 of \Coq{} is based on the V5.10 architecture. It -was ported to the new language Objective Caml by Bruno Barras. The +was ported to the new language {\ocaml} by Bruno Barras. The underlying framework has slightly changed and allows more conversions between sorts. @@ -564,7 +564,7 @@ unresolved implicit has been implemented by Hugo Herbelin. Laurent Théry's contribution on strings and Pierre Letouzey and Jean-Christophe Filliâtre's contribution on finite maps have been integrated to the {\Coq} standard library. Pierre Letouzey developed a -library about finite sets ``à la Objective Caml''. With Jean-Marc +library about finite sets ``à la {\ocaml}''. With Jean-Marc Notin, he extended the library on lists. Pierre Letouzey's contribution on rational numbers has been integrated and extended.. |