aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/declarations.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 1dc4a7cb8..4cfb3e2ab 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,7 +8,7 @@ open Term
open Sign
(*i*)
-(*s Constants (internal representation). *)
+(*s Constants (internal representation) (Definition/Axiom) *)
type lazy_constant_value =
| Cooked of constr