Update expected output

mtzguido · Feb 9, 2025 · b222e58 · b222e58
1 parent fcdab71
commit b222e58
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/tests/error-messages/DesugarOrder.fst.json_output.expected b/tests/error-messages/DesugarOrder.fst.json_output.expected
@@ -1,3 +1,3 @@
 >> Got issues: [
-{"msg":["Identifier not found: [a]"],"level":"Error","range":{"def":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}},"use":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}}},"number":72,"ctx":["While desugaring module DesugarOrder"]}
+{"msg":["Identifier not found: a"],"level":"Error","range":{"def":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}},"use":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}}},"number":72,"ctx":["While desugaring module DesugarOrder"]}
 >>]
diff --git a/tests/error-messages/DesugarOrder.fst.output.expected b/tests/error-messages/DesugarOrder.fst.output.expected
@@ -1,5 +1,5 @@
 >> Got issues: [
 * Error 72 at DesugarOrder.fst(7,12-7,13):
-  - Identifier not found: [a]
+  - Identifier not found: a
 
 >>]
diff --git a/tests/ide/emacs/Backtracking.refinements.ideout.expected b/tests/ide/emacs/Backtracking.refinements.ideout.expected
@@ -33,8 +33,8 @@
 {"kind": "response", "query-id": "32", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [5, 8], "end": [5, 8], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "33", "response": [], "status": "success"}
 {"kind": "response", "query-id": "34", "response": [], "status": "success"}
-{"kind": "response", "query-id": "35", "response": [{"level": "error", "message": "- Identifier not found: [b]\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": "<input>"}]}], "status": "success"}
-{"kind": "response", "query-id": "36", "response": [{"level": "error", "message": "- Identifier not found: [b]\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "35", "response": [{"level": "error", "message": "- Identifier not found: b\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "36", "response": [{"level": "error", "message": "- Identifier not found: b\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "37", "response": [[3, "Prims", "nat"], [0, "<search term>", "nat"]], "status": "success"}
 {"kind": "response", "query-id": "38", "response": [], "status": "success"}
 {"kind": "response", "query-id": "39", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [5, 15], "end": [5, 15], "fname": "<input>"}]}], "status": "success"}

diff --git a/tests/ide/emacs/Harness.selfref.ideout.expected b/tests/ide/emacs/Harness.selfref.ideout.expected
@@ -1,4 +1,4 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Could not prove post-condition\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also <input>(1,25-1,32)\n", "number": 19, "ranges": [{"beg": [1, 35], "end": [1, 37], "fname": "<input>"}, {"beg": [1, 25], "end": [1, 32], "fname": "<input>"}]}], "status": "failure"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Identifier not found: [Harness.always_foo]\n- Module Harness resolved into Harness, which does not belong to the list of\n  modules in scope, namely:\n    FStar.Mul, FStar.Classical, FStar.Classical.Sugar, FStar.Pervasives,\n    FStar.Pervasives.Native, Prims\n", "number": 72, "ranges": [{"beg": [1, 43], "end": [1, 53], "fname": "<input>"}]}], "status": "failure"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Module name Harness resolved to Harness which is not in scope.\n", "number": 72, "ranges": [{"beg": [1, 35], "end": [1, 42], "fname": "<input>"}]}], "status": "failure"}