summaryrefslogtreecommitdiffstats
path: root/transp-inf110-03-quantif.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-03-quantif.tex')
-rw-r--r--transp-inf110-03-quantif.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 07c5d43..61063b9 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -542,7 +542,7 @@ monde des démonstrations, plus simples, ou différentes.
\medskip
-\itempoint En Coq, les deux mondes sont \alert{séparés mais
+\itempoint En Coq/Rocq, les deux mondes sont \alert{séparés mais
parallèles} : $\mathit{Prop}$ pour le type des propositions et
$\mathit{Type}$ pour le type des types d'individus.