diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml index a7a300f5c487ad73a27bff923e679e3dc9298cbb..b079330d0ef0a6dc51ea6b1b3f75a75ac76f004e 100644 --- a/src/kernel_services/parsetree/logic_ptree.ml +++ b/src/kernel_services/parsetree/logic_ptree.ml @@ -245,7 +245,7 @@ and decl_node = (** [LDaxiomatic(id,decls)] represents a block of axiomatic definitions.*) | LDmodule of string * decl list - (** [LDaxiomatic(id,decls)] + (** [LDmodule(id,decls)] represents a module of axiomatic definitions.*) | LDimport of string option * string * string option (** [LDimport(driver,module,alias)]