aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/hidden-files3
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index a2bc90ffc0..dbc3a42ee9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -12,18 +12,21 @@ plugins/extraction/ExtrHaskellZInteger.v
plugins/extraction/ExtrHaskellZNum.v
plugins/extraction/ExtrOcamlBasic.v
plugins/extraction/ExtrOcamlBigIntConv.v
+plugins/extraction/ExtrOcamlChar.v
plugins/extraction/ExtrOCamlInt63.v
plugins/extraction/ExtrOCamlFloats.v
plugins/extraction/ExtrOcamlIntConv.v
plugins/extraction/ExtrOcamlNatBigInt.v
plugins/extraction/ExtrOcamlNatInt.v
plugins/extraction/ExtrOcamlString.v
+plugins/extraction/ExtrOcamlNativeString.v
plugins/extraction/ExtrOcamlZBigInt.v
plugins/extraction/ExtrOcamlZInt.v
plugins/extraction/Extraction.v
plugins/funind/FunInd.v
plugins/funind/Recdef.v
plugins/ltac/Ltac.v
+plugins/micromega/Ztac.v
plugins/micromega/DeclConstant.v
plugins/micromega/Env.v
plugins/micromega/EnvRing.v