output changed!?!?

FStarLang · Oct 11, 2024 · 9b0b21c · 9b0b21c
1 parent 91c1f28
commit 9b0b21c
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/tests/error-messages/Bug2899.fst.expected b/tests/error-messages/Bug2899.fst.expected
@@ -2,8 +2,8 @@
 * Error 170 at Bug2899.fst(7,12-7,18):
   - Tactic failed
   - Tactic got stuck!
-  - Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ())
-      "(((proofstate)))"
+  - Reduction stopped at:
+      FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))"
   - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
   - See also FStar.Tactics.Effect.fsti(212,48-212,58)
 
@@ -21,8 +21,8 @@
 * Error 170 at Bug2899.fst(13,12-13,18):
   - Tactic failed
   - Tactic got stuck!
-  - Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())
-      "(((proofstate)))"
+  - Reduction stopped at:
+      FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))"
   - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
   - See also FStar.Tactics.Effect.fsti(212,48-212,58)
 

diff --git a/tests/error-messages/Bug2899.fst.json_expected b/tests/error-messages/Bug2899.fst.json_expected
@@ -1,11 +1,11 @@
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ())\n  \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
 >>]
 >> Got issues: [
 {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
 >>]
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())\n  \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
 >>]
 >> Got issues: [
 {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}