Update expected output

Now mentions Stubs
FStarLang · Nov 27, 2023 · d0ac978 · d0ac978
1 parent 117a847
commit d0ac978
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 35 deletions.
diff --git a/tests/error-messages/Bug2899.fst.expected b/tests/error-messages/Bug2899.fst.expected
@@ -2,7 +2,7 @@
 * Error 170 at Bug2899.fst(7,12-7,18):
   - Tactic failed
   - Tactic got stuck!
-  - Reduction stopped at: FStar.Tactics.Result.Success (Prims.admit ())
+  - 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,7 +21,7 @@
 * Error 170 at Bug2899.fst(13,12-13,18):
   - Tactic failed
   - Tactic got stuck!
-  - Reduction stopped at: FStar.Tactics.V2.Builtins.dump (Prims.admit ())
+  - 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/WPExtensionality.fst.expected b/tests/error-messages/WPExtensionality.fst.expected
@@ -6,84 +6,84 @@
 
 >>]
 * Warning 288 at WPExtensionality.fst(25,2-25,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(30,13-30,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(36,2-36,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(41,13-41,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(47,2-47,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(53,13-53,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(59,2-59,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(65,13-65,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(71,2-71,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(76,13-76,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(82,2-82,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(87,13-87,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(93,2-93,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(99,13-99,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(105,2-105,8):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 * Warning 288 at WPExtensionality.fst(111,13-111,20):
-  - FStar.Reflection.V2.Builtins.term_eq is deprecated
+  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
   - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)
+  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
 
 Verified module: WPExtensionality
 All verification conditions discharged successfully
diff --git a/tests/ide/emacs/fstarmode_gh73.out.expected b/tests/ide/emacs/fstarmode_gh73.out.expected
@@ -1,5 +1,5 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Adding an implicit 'assume new' qualifier on document\n", "number": 239, "ranges": [{"beg": [36, 5], "end": [36, 13], "fname": "FStar.Stubs.Pprint.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [616, 15], "end": [616, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Pattern uses these theory symbols or terms that should not be in an smt pattern:  Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
+{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [150, 0], "end": [150, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [150, 0], "end": [150, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Adding an implicit 'assume new' qualifier on document\n", "number": 239, "ranges": [{"beg": [36, 5], "end": [36, 13], "fname": "FStar.Stubs.Pprint.fsti"}]}, {"level": "warning", "message": "  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)\n", "number": 288, "ranges": [{"beg": [616, 15], "end": [616, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [150, 0], "end": [150, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [150, 0], "end": [150, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Pattern uses these theory symbols or terms that should not be in an smt pattern:  Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "  - Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "  - Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}