diff --git a/doc/code/toc_head.htm b/doc/code/toc_head.htm
index 6f2399a0e1213dac2b272584a6b43b05366cb02d..6ff68d3c7edb84cf5688961d1128fb6ce374425d 100644
--- a/doc/code/toc_head.htm
+++ b/doc/code/toc_head.htm
@@ -20,12 +20,12 @@
<!-- -->
<!---------------------------------------------------------------------------->
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<!DOCTYPE html>
<html>
<head>
<title>Frama-C API</title>
<link rel="stylesheet" href="style.css" type="text/css">
-<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
+<meta charset="utf-8">
</head>
<body>
<h1>Frama-C API Documentation</h1>
diff --git a/doc/developer/TODO b/doc/developer/TODO
deleted file mode 100644
index 489e0e1eebfc19d2b2b4009d7afda72c794fead4..0000000000000000000000000000000000000000
--- a/doc/developer/TODO
+++ /dev/null
@@ -1,43 +0,0 @@
-=========
-TODO-list
-=========
-
-Advance
-=======
-
-* Configure.in
- o Principle: manque les --static ou --dynamic
- o --external-plugin (Virgile, bts#203)
-
-* Command Line Options
- o possibility of customisation through optional functor parameters
-
-* Types as first class values
-
-* Journalisation
- [advanced plugin development]
- o lien avec les exemples de chargement dynamique
- [refman]
- o spécification du module "Type" dans répertoire "lib":
- ajouté un lien vers Section "Journalisation" quand cette
- dernière sera écrite.
-
-* Documentation des sources:
- o test d'intégrité du code wrt plugin dev guide
-
-* GUI:
- o améliorer la doc: mieux expliquer comment utiliser les hooks pour coder
- les parties similaires à chaque greffon (panneau latéral, etc).
- o GUI des greffons dynamiques
-
-Refman
-======
-
-* Figure des makefiles:
- o ajouter le fait que Makefile.dynamic est généré à partir de
- Makefile.dynamic.internal/external
-
-* Makefile.dynamic: ce qui lui est spécifique
-
-List of recommendations (?)
-=======================
diff --git a/doc/index.html b/doc/index.html
index 67520447c419c95d4faca4fc20d469b793d83318..477af4ab0783b659f564dda1aa1e19ece764820e 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -1,10 +1,8 @@
-<!DOCTYPE html
-PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
-"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<!DOCTYPE html>
<html>
<head>
-<meta http-equiv="Content-Type" content="text/xhtml; charset=utf-8"/>
+<meta charset="utf-8">
<link rel="stylesheet" href="style.css" type="text/css"/>
<title>Frama-C</title>
</head>
diff --git a/doc/makeLatex b/doc/makeLatex
index c0414b80e350006f150b066e500f4afddf609f94..abcd85df97cf381080aa0ecbcea9b005930f6174 100644
--- a/doc/makeLatex
+++ b/doc/makeLatex
@@ -1,22 +1,22 @@
-# Fichier à inclure dans son makefile pour faire des compilation latex.
-# L'utilisateur doit définir certaines variables (notées +)
-# et peut en option en (re)définir d'autres (notées *) :
+# Fichier à inclure dans son makefile pour faire des compilation latex.
+# L'utilisateur doit définir certaines variables (notées +)
+# et peut en option en (re)définir d'autres (notées *) :
#
-# === outils (peuvent être redéfinis si on veut préciser le path par exemple) :
+# === outils (peuvent être redéfinis si on veut préciser le path par exemple) :
# TEXI (= texi2dvi)
# HEVEA (HEVEAOPTS), HACHA
# === fichiers :
-# * TOPTEX=top.tex : déterminé par défaut par un grep de documentclass
-# * GENERATED_TEX= : fichiers .tex générés (vide par défaut)
+# * TOPTEX=top.tex : déterminé par défaut par un grep de documentclass
+# * GENERATED_TEX= : fichiers .tex générés (vide par défaut)
#
# * FIGURES_TODO= : noms de figures sans extension (-> .eps + .pdf)
# (suppose qu'on a le .eps et le .pdf
# ou qu'on sait a une cible pour les fabriquer...)
#
-# * HVA=macros.hva : si on a besoin de définir des choses pour hevea
+# * HVA=macros.hva : si on a besoin de définir des choses pour hevea
#
-# Les figures (fichiers .fig) sont compilés en postscript et/ou en pdf
+# Les figures (fichiers .fig) sont compilés en postscript et/ou en pdf
# en fonction des besoins. Si on souhaite compiler une figure en latex
# (formules, etc) il faut simplement nommer le fichier *.tex.fig
#
@@ -25,14 +25,14 @@
# debug_latex,
# clean_latex, clean_hevea, clean
#
-# loop : lance gv sur TOPTEX.ps et une boucle de compilation qui met à jour
-# le contenu visualisé.
-# Il est conseillé d'utiliser plutôt la cible 'sloop' pour ne pas avoir
-# un écran qui défile en permanence.
+# loop : lance gv sur TOPTEX.ps et une boucle de compilation qui met à jour
+# le contenu visualisé.
+# Il est conseillé d'utiliser plutôt la cible 'sloop' pour ne pas avoir
+# un écran qui défile en permanence.
#------------------------------------------------------------------------------
-# l'avantage de texi2dvi par rapport à latex,
+# l'avantage de texi2dvi par rapport à latex,
# c'est qu'il s'occupe de l'index, de la biblio,
# et de lancer latex autant de fois qu'il le faut.
TEXI?=texi2dvi
@@ -73,13 +73,13 @@ FIGURES_EPS = $(SIMPLE_FIGURES_EPS) $(FIGURES_PSTEX)
FIGURES_PDF = $(SIMPLE_FIGURES_PDF) $(FIGURES_PDFTEX)
GENERATED_FIGURES = $(FIGURES_EPS) $(FIGURES_PDF) $(FIGURES_TEX)
-# plus utile : hevea se débrouille tout seul.
+# plus utile : hevea se débrouille tout seul.
#IMAGES_GIF = $(shell grep -s gif $(SRC).html | grep "^[ ]*<IMG" | sed -e 's=[^"]*"\(.*.gif\).*=\1=')
-# TODO : à étendre au cas d'une biblio multiple (plusieurs fichiers .bib).
+# TODO : à étendre au cas d'une biblio multiple (plusieurs fichiers .bib).
BIB_NAME = $(shell grep -h "bibliography{" $(TOPTEX) \
| sed -e 's/\\bibliography{\(.*\)}/\1.bib/')
-# TODO: à modifier pour chercher dans BIBINPUTS
+# TODO: Ã modifier pour chercher dans BIBINPUTS
ifneq ($(strip $(BIB_NAME)),)
BIB_FILE = $(BIB_NAME)
@@ -115,7 +115,7 @@ debug_latex :
@echo "HVA = $(HVA)"
#------------------------------------------------------------------------------
-# Dépendances :
+# Dépendances :
$(SRC).dvi : $(ALL_TEX) $(FIGURES_TEX) $(FIGURES_EPS) $(BBL_FILE) $(FIGURES_PDF)
# no <TAB> here
@@ -129,7 +129,7 @@ $(SRC).html : $(ALL_TEX) $(SRC).pdf $(SRC).bbl
#------------------------------------------------------------------------------
# Regles de production :
-# dessins .eps à partir des .fig de xfig
+# dessins .eps à partir des .fig de xfig
%.eps : %.tex.fig
fig2dev -L pstex $< $@
@@ -160,7 +160,7 @@ $(SRC).html : $(ALL_TEX) $(SRC).pdf $(SRC).bbl
$(TEXI2DVI) $<
$(SRC).bbl : $(BIB_FILE)
- @echo "=== Fichier .bib plus récent -> effacement du .bbl"
+ @echo "=== Fichier .bib plus récent -> effacement du .bbl"
rm -f $(SRC).bbl
@@ -193,9 +193,9 @@ $(SRC).html: $(HVA) $(SRC).tex
index.html: $(SRC).html
$(HACHA) -o index.html $(SRC).html
-# ceci n'est normalement plus utile sous UNIX grace à l'option -fix de hevea
+# ceci n'est normalement plus utile sous UNIX grace à l'option -fix de hevea
#$(IMAGES_GIF) : $(SRC).image.tex
- #@echo "=== Génération des images gif"
+ #@echo "=== Génération des images gif"
#imagen $(SRC)
#------------------------------------------------------------------------------
@@ -228,14 +228,14 @@ sloop:
#------------------------------------------------------------------------------
clean_hevea :
- @echo "=== Ménage des fichiers hevea"
+ @echo "=== Ménage des fichiers hevea"
rm -f $(SRC).html $(SRC).h{toc,aux,ind,idx} $(SRC).cb
rm -f index.html $(SRC)[0-9][0-9][0-9].html $(SRC).css
rm -f $(SRC).image.cb $(SRC).image.tex $(SRC)[0-9][0-9][0-9].gif
rm -f previous_motif.gif next_motif.gif contents_motif.gif
clean_tmp_tex :
- @echo "=== Ménage des fichiers temporaires de latex"
+ @echo "=== Ménage des fichiers temporaires de latex"
rm -f $(SRC).aux
rm -f $(SRC).log
rm -f $(SRC).blg
@@ -249,12 +249,12 @@ clean_tmp_tex :
rm -f $(SRC).out
clean_latex : clean_tmp_tex
- @echo "=== Ménage des fichiers latex"
+ @echo "=== Ménage des fichiers latex"
rm -f $(SRC).bbl
rm -f $(SRC).dvi
rm -f $(SRC).ps
rm -f $(SRC).pdf
- @echo "=== Ménage des figures"
+ @echo "=== Ménage des figures"
rm -f *.~[0-9]*~ *.bak *~
rm -f $(GENERATED_FIGURES)
diff --git a/doc/training/developer/macros.tex b/doc/training/developer/macros.tex
index 752a31d04f66dd6985285c08fd970c08074888c9..3fa1075aa128396fd04415dab6710550dc1c3dbe 100644
--- a/doc/training/developer/macros.tex
+++ b/doc/training/developer/macros.tex
@@ -40,7 +40,7 @@ literate=%
{'a}{$\alpha$}1%
{'b}{$\beta$}1%
{'c}{$\gamma$}1%
-{µ}{`{}}1%
+{µ}{`{}}1%
}
\newcommand{\framac}{\textsl{Frama-C}\xspace}
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index b862113e233ab815b47e1b9b737147d4cda36bc3..a76f594e99b63ab1008d338ef1e0ad077cc76401 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -286,13 +286,11 @@ let dump_acsl_stats fmt =
let dump_acsl_stats_html fmt =
Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.fprintf fmt
- "@[<v 0> <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
- \"http://www.w3.org/TR/html4/strict.dtd\">@ \
+ "@[<v 0> <!DOCTYPE html>@ \
@{<html>@ \
@{<head>@ \
@{<title>%s@}@ \
- <meta content=\"text/html; charset=iso-8859-1\" \
- http-equiv=\"Content-Type\"/>@ \
+ <meta charset=\"utf-8\">@ \
@{<style type=\"text/css\">%s@}@ \
@}@ \
@{<body>\
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index ca8f10f76308ae96c36036a4017f95f43b5bb9b6..d24f3cefc65855a44c6f4132f1fd677b4e12d243 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -609,13 +609,11 @@ let dump_html fmt cil_visitor =
(fun fmt cil_visitor -> cil_visitor#print_stats fmt) cil_visitor
in
Format.fprintf fmt "@[<v 0>\
- <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
- \"http://www.w3.org/TR/html4/strict.dtd\">@ \
+ <!DOCTYPE html>@ \
@{<html>@ \
@{<head>@ \
@{<title>%s@}@ \
- <meta content=\"text/html; charset=iso-8859-1\" \
- http-equiv=\"Content-Type\"/>@ \
+ <meta charset=\"utf-8\">@ \
@{<style type=\"text/css\">%s@}@ \
@}@ \
@{<body>\
diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
index 230de710f3bed354453441f7ffb9a8a44acbe7fb..7ba8654c6b8886c4ce8964e98b2d2f7621eeb504 100644
--- a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
+++ b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
@@ -277,7 +277,7 @@ let start_html_page modname =
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
-<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\" />
+<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
<title>Module %s</title>
<meta name=\"description\" content=\"Documentation of Coq module %s\" />
<link href=\"coq2html.css\" rel=\"stylesheet\" type=\"text/css\" />
diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/head.html b/src/plugins/wp/doc/coqdoc/coq2tex/head.html
index 2142d3ee5c6a6e561ae0d62051894ba95ab0caa1..d691cc325b62c43cf7e218939ae95de28fc8fb6d 100644
--- a/src/plugins/wp/doc/coqdoc/coq2tex/head.html
+++ b/src/plugins/wp/doc/coqdoc/coq2tex/head.html
@@ -1,8 +1,8 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
+<!DOCTYPE html>
+<html>
<head>
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
+<meta charset="utf-8">
<title>Frama-C WP Coq Library</title>
<meta name="description" content="Documentation of Coq modules for Frama-C WP" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
diff --git a/src/plugins/wp/doc/coqdoc/coqdoc.sty b/src/plugins/wp/doc/coqdoc/coqdoc.sty
index 9de9a38ff9a720d1daf6313e25b20daa2bd9e0a1..f49f9f0066a1d61dc8d0c5809bb2a67dfd71ba10 100644
--- a/src/plugins/wp/doc/coqdoc/coqdoc.sty
+++ b/src/plugins/wp/doc/coqdoc/coqdoc.sty
@@ -1,5 +1,5 @@
-% This is coqdoc.sty, by Jean-Christophe Filliâtre
+% This is coqdoc.sty, by Jean-Christophe Filliâtre
% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
%
% You can modify the following macros to customize the appearance