Update error messages

Author: clementblaudeau

hax-types/src/diagnostics/mod.rs

@@ -16,17 +16,13 @@ pub struct Diagnostics {
 impl std::fmt::Display for Diagnostics {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         match &self.kind {
-            Kind::Unimplemented { issue_id, details } => write!(
+            Kind::Unimplemented { issue_id:_, details } => write!(
                 f,
-                "something is not implemented yet.{}{}",
-                match issue_id {
-                    Some(id) => format!("This is discussed in issue https://github.com/hacspec/hax/issues/{id}.\nPlease upvote or comment this issue if you see this error message."),
-                    _ => "".to_string(),
-                },
+                "something is not implemented yet.{}",
                 match details {
                     Some(details) => format!("\n{}", details),
                     _ => "".to_string(),
-                }
+                },
             ),
             Kind::UnsupportedMacro { id } => write!(
                 f,

rust-engine/src/printer/pretty_ast.rs

@@ -114,8 +114,8 @@ impl<'a, 'b, A: 'a + Clone, P: PrettyAst<'a, 'b, A>, T: 'b + serde::Serialize> P
 /// ## Examples:
 /// - `todo_document!(allocator)`
 /// - `todo_document!(allocator, "This is a todo")`
-/// - `todo_document!(allocator, issue #42)`
-/// - `todo_document!(allocator, issue #42, "This is a todo")`
+/// - `todo_document!(allocator, issue 42)`
+/// - `todo_document!(allocator, issue 42, "This is a todo")`
 macro_rules! todo_document {
     ($allocator:ident, issue $issue:literal) => {
         {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), Some($issue));}