aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-07-26 20:50:58 +0200
committerPierre-Marie Pédrot2017-07-26 20:59:49 +0200
commit57b9df4e07351a753f897dc24eb8238f6465b26d (patch)
tree6b9e29bc4a53a7b4ede6d15739a3c4cce200f1d9 /_CoqProject
parente917841e46264ad7b80241b25dcd7731eca468a8 (diff)
Dedicated module for ident type.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 6d3470cfa7..2561b7b6ec 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -23,6 +23,7 @@ src/ltac2_plugin.mlpack
theories/Init.v
theories/Int.v
theories/String.v
+theories/Ident.v
theories/Array.v
theories/Control.v
theories/Message.v