Update expected output

Char type moved
FStarLang · Jan 13, 2025 · 58693ea · 58693ea
1 parent 87369fa
commit 58693ea
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/tests/error-messages/ExpectFailure.fst.json_output.expected b/tests/error-messages/ExpectFailure.fst.json_output.expected
@@ -1,8 +1,8 @@
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":15},"end_pos":{"line":28,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":8},"end_pos":{"line":28,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
@@ -11,11 +11,11 @@
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":15},"end_pos":{"line":30,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":8},"end_pos":{"line":30,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
diff --git a/tests/error-messages/ExpectFailure.fst.output.expected b/tests/error-messages/ExpectFailure.fst.output.expected
@@ -2,14 +2,14 @@
 * Error 189 at ExpectFailure.fst(20,12-20,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(24,12-24,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
@@ -32,20 +32,20 @@
 * Error 189 at ExpectFailure.fst(43,12-43,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(50,12-50,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(61,12-61,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]