diff --git a/examples/dm4free/delimcc.fst b/examples/dm4free/DelimCC.fst
similarity index 100%
rename from examples/dm4free/delimcc.fst
rename to examples/dm4free/DelimCC.fst
diff --git a/examples/metatheory/indind.fst b/examples/metatheory/IndInd.fst
similarity index 99%
rename from examples/metatheory/indind.fst
rename to examples/metatheory/IndInd.fst
index 0289c487117..dbd3e82523a 100644
--- a/examples/metatheory/indind.fst
+++ b/examples/metatheory/IndInd.fst
@@ -13,7 +13,7 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-module Indind
+module IndInd
 
 /// Induction-induction can be encoded in F* at least up to simple
 /// elimination (see Forsberg ...)
diff --git a/examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst b/examples/paradoxes/PropImpredicativeAndNonStrictlyPositiveInductives.fst
similarity index 100%
rename from examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst
rename to examples/paradoxes/PropImpredicativeAndNonStrictlyPositiveInductives.fst
diff --git a/examples/rel/label.fst b/examples/rel/Label.fst
similarity index 100%
rename from examples/rel/label.fst
rename to examples/rel/Label.fst
diff --git a/examples/termination/maxime.fst b/examples/termination/Maxime.fst
similarity index 100%
rename from examples/termination/maxime.fst
rename to examples/termination/Maxime.fst
diff --git a/examples/termination/mcCarthy91.fst b/examples/termination/McCarthy91.fst
similarity index 100%
rename from examples/termination/mcCarthy91.fst
rename to examples/termination/McCarthy91.fst
diff --git a/examples/termination/termination.fst b/examples/termination/Termination.fst
similarity index 100%
rename from examples/termination/termination.fst
rename to examples/termination/Termination.fst
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
index 40bb2021e55..2e7a26b4388 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
@@ -910,16 +910,18 @@ let (check_module_declaration_against_filename :
   FStar_Ident.lident -> Prims.string -> unit) =
   fun lid ->
     fun filename ->
-      let k' = lowercase_join_longident lid true in
+      let k' = string_of_lid lid true in
       let uu___ =
-        let uu___1 =
-          let uu___2 =
-            let uu___3 =
-              let uu___4 = FStar_Compiler_Util.basename filename in
-              check_and_strip_suffix uu___4 in
-            FStar_Compiler_Util.must uu___3 in
-          FStar_Compiler_String.lowercase uu___2 in
-        uu___1 <> k' in
+        (let uu___1 =
+           let uu___2 =
+             let uu___3 = FStar_Compiler_Util.basename filename in
+             check_and_strip_suffix uu___3 in
+           FStar_Compiler_Util.must uu___2 in
+         uu___1 <> k') &&
+          (let uu___1 =
+             let uu___2 = FStar_Compiler_Util.basename filename in
+             uu___2 = "prims.fst" in
+           Prims.op_Negation uu___1) in
       if uu___
       then
         let uu___1 =
@@ -927,10 +929,15 @@ let (check_module_declaration_against_filename :
             let uu___3 =
               let uu___4 = string_of_lid lid true in
               FStar_Compiler_Util.format2
-                "The module declaration \"module %s\" found in file %s does not match its filename. Dependencies will be incorrect and the module will not be verified."
+                "The module declaration \"module %s\" found in file %s does not match its filename."
                 uu___4 filename in
             FStar_Errors_Msg.text uu___3 in
-          [uu___2] in
+          let uu___3 =
+            let uu___4 =
+              FStar_Errors_Msg.text
+                "Dependencies will be incorrect and the module will not be verified." in
+            [uu___4] in
+          uu___2 :: uu___3 in
         FStar_Errors.log_issue FStar_Ident.hasrange_lident lid
           FStar_Errors_Codes.Error_ModuleFileNameMismatch ()
           (Obj.magic FStar_Errors_Msg.is_error_message_list_doc)
diff --git a/ocaml/fstar-lib/generated/FStar_Universal.ml b/ocaml/fstar-lib/generated/FStar_Universal.ml
index 7d94dd1b872..8eb8fe94bb9 100644
--- a/ocaml/fstar-lib/generated/FStar_Universal.ml
+++ b/ocaml/fstar-lib/generated/FStar_Universal.ml
@@ -203,13 +203,22 @@ let (parse :
                                    FStar_ToSyntax_Interleave.interleave_module
                                      ast true in
                                  with_dsenv_of_env env1 uu___8)
+                        | (FStar_Parser_AST.Interface (lid1, uu___5, uu___6),
+                           FStar_Parser_AST.Module (lid2, uu___7)) ->
+                            FStar_Errors.raise_error
+                              FStar_Ident.hasrange_lident lid1
+                              FStar_Errors_Codes.Fatal_PreModuleMismatch ()
+                              (Obj.magic
+                                 FStar_Errors_Msg.is_error_message_string)
+                              (Obj.magic
+                                 "Module name in implementation does not match that of interface.")
                         | uu___5 ->
                             FStar_Errors.raise_error0
                               FStar_Errors_Codes.Fatal_PreModuleMismatch ()
                               (Obj.magic
                                  FStar_Errors_Msg.is_error_message_string)
                               (Obj.magic
-                                 "mismatch between pre-module and module"))) in
+                                 "Module name in implementation does not match that of interface."))) in
             (match uu___2 with
              | (ast1, env1) ->
                  let uu___3 = FStar_ToSyntax_ToSyntax.ast_modul_to_modul ast1 in
diff --git a/src/fstar/FStar.Universal.fst b/src/fstar/FStar.Universal.fst
index 6b305ae3ce5..f5b0c521e0c 100644
--- a/src/fstar/FStar.Universal.fst
+++ b/src/fstar/FStar.Universal.fst
@@ -103,8 +103,17 @@ let parse (env:uenv) (pre_fn: option string) (fn:string)
             with_dsenv_of_env env (FStar.ToSyntax.Interleave.initialize_interface lid1 decls1)
           in
           with_dsenv_of_env env (FStar.ToSyntax.Interleave.interleave_module ast true)
+
+        | Parser.AST.Interface (lid1, _, _), Parser.AST.Module (lid2, _) ->
+          (* Names do not match *)
+          Errors.raise_error lid1
+            Errors.Fatal_PreModuleMismatch
+            "Module name in implementation does not match that of interface."
+
         | _ ->
-            Errors.raise_error0 Errors.Fatal_PreModuleMismatch "mismatch between pre-module and module"
+          Errors.raise_error0
+            Errors.Fatal_PreModuleMismatch
+            "Module name in implementation does not match that of interface."
   in
   with_dsenv_of_env env (Desugar.ast_modul_to_modul ast)
 
diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst
index 602cc7c56b1..d3afd007f91 100644
--- a/src/parser/FStar.Parser.Dep.fst
+++ b/src/parser/FStar.Parser.Dep.fst
@@ -514,12 +514,14 @@ let namespace_of_lid l =
   String.concat "_" (List.map string_of_id (ns_of_lid l))
 
 let check_module_declaration_against_filename (lid: lident) (filename: string): unit =
-  let k' = lowercase_join_longident lid true in
-  if String.lowercase (must (check_and_strip_suffix (basename filename))) <> k' then
+  let k' = string_of_lid lid true in
+  if must (check_and_strip_suffix (basename filename)) <> k'
+     && (not (basename filename = "prims.fst")) (* Exception for module Prims = prims.fst until we switch *)
+  then
     log_issue lid Errors.Error_ModuleFileNameMismatch [
         Errors.Msg.text (Util.format2 "The module declaration \"module %s\" \
-          found in file %s does not match its filename. Dependencies will be \
-          incorrect and the module will not be verified." (string_of_lid lid true) filename)
+          found in file %s does not match its filename." (string_of_lid lid true) filename);
+        Errors.Msg.text "Dependencies will be incorrect and the module will not be verified.";
       ]
 
 exception Exit
diff --git a/tests/bug-reports/Bug1347b.fst b/tests/bug-reports/Bug1347b.fst
index f99711f42a0..337738d0fb0 100644
--- a/tests/bug-reports/Bug1347b.fst
+++ b/tests/bug-reports/Bug1347b.fst
@@ -13,7 +13,7 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-module Bug1347B
+module Bug1347b
 
 open FStar.Tactics.V2
 
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
index ff6c7c0439f..1c5ed101806 100644
--- a/tests/bug-reports/Makefile
+++ b/tests/bug-reports/Makefile
@@ -35,7 +35,7 @@ SHOULD_VERIFY_CLOSED=\
 	UnificationCrash.fst Bug1150.fst Bug1076.fst Bug1341.fst Bug1345.fst		\
 	Bug1345b.fst Bug1345c.fst Bug1346.fst Bug1348.fst Bug1362.fst			\
 	Bug1347b.fst Bug1206.fst Bug1271.fst Bug1305.fst Bug1361.fst Bug1383.fst	\
-	Bug1414.fst unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst		\
+	Bug1414.fst Unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst		\
 	Bug1352.fst Bug1123.fst ScopeOfBinderGuard.fst Bug1319a.fst Bug1319b.fst	\
 	Bug1319c.fst Bug1319d.fst Bug1319e.fst Bug1319f.fst Bug807a.fst			\
 	Bug807b.fst Bug807c.fst Bug807d.fst Bug807e.fst Bug1502.fst Bug1488.fst		\
diff --git a/tests/bug-reports/unfold.fst b/tests/bug-reports/Unfold.fst
similarity index 100%
rename from tests/bug-reports/unfold.fst
rename to tests/bug-reports/Unfold.fst
diff --git a/tests/bug-reports/unfold.fst.hints b/tests/bug-reports/Unfold.fst.hints
similarity index 100%
rename from tests/bug-reports/unfold.fst.hints
rename to tests/bug-reports/Unfold.fst.hints
diff --git a/tests/ide/emacs/backtracking.fst b/tests/ide/emacs/Backtracking.fst
similarity index 100%
rename from tests/ide/emacs/backtracking.fst
rename to tests/ide/emacs/Backtracking.fst
diff --git a/tests/ide/emacs/backtracking.peek-with-unset-module.in b/tests/ide/emacs/Backtracking.peek-with-unset-module.in
similarity index 100%
rename from tests/ide/emacs/backtracking.peek-with-unset-module.in
rename to tests/ide/emacs/Backtracking.peek-with-unset-module.in
diff --git a/tests/ide/emacs/backtracking.peek-with-unset-module.out.expected b/tests/ide/emacs/Backtracking.peek-with-unset-module.out.expected
similarity index 100%
rename from tests/ide/emacs/backtracking.peek-with-unset-module.out.expected
rename to tests/ide/emacs/Backtracking.peek-with-unset-module.out.expected
diff --git a/tests/ide/emacs/backtracking.refinements.in b/tests/ide/emacs/Backtracking.refinements.in
similarity index 100%
rename from tests/ide/emacs/backtracking.refinements.in
rename to tests/ide/emacs/Backtracking.refinements.in
diff --git a/tests/ide/emacs/backtracking.refinements.out.expected b/tests/ide/emacs/Backtracking.refinements.out.expected
similarity index 100%
rename from tests/ide/emacs/backtracking.refinements.out.expected
rename to tests/ide/emacs/Backtracking.refinements.out.expected
diff --git a/tests/ide/emacs/fstarmode_gh73.fst b/tests/ide/emacs/FStarMode_GH73.fst
similarity index 100%
rename from tests/ide/emacs/fstarmode_gh73.fst
rename to tests/ide/emacs/FStarMode_GH73.fst
diff --git a/tests/ide/emacs/fstarmode_gh73.in b/tests/ide/emacs/FStarMode_GH73.in
similarity index 100%
rename from tests/ide/emacs/fstarmode_gh73.in
rename to tests/ide/emacs/FStarMode_GH73.in
diff --git a/tests/ide/emacs/fstarmode_gh73.out.expected b/tests/ide/emacs/FStarMode_GH73.out.expected
similarity index 100%
rename from tests/ide/emacs/fstarmode_gh73.out.expected
rename to tests/ide/emacs/FStarMode_GH73.out.expected
diff --git a/tests/ide/emacs/fib.compute.in b/tests/ide/emacs/Fib.compute.in
similarity index 100%
rename from tests/ide/emacs/fib.compute.in
rename to tests/ide/emacs/Fib.compute.in
diff --git a/tests/ide/emacs/fib.compute.out.expected b/tests/ide/emacs/Fib.compute.out.expected
similarity index 100%
rename from tests/ide/emacs/fib.compute.out.expected
rename to tests/ide/emacs/Fib.compute.out.expected
diff --git a/tests/ide/emacs/fib.fst b/tests/ide/emacs/Fib.fst
similarity index 100%
rename from tests/ide/emacs/fib.fst
rename to tests/ide/emacs/Fib.fst
diff --git a/tests/ide/emacs/infotable.fst b/tests/ide/emacs/InfoTable.fst
similarity index 100%
rename from tests/ide/emacs/infotable.fst
rename to tests/ide/emacs/InfoTable.fst
diff --git a/tests/ide/emacs/infotable.lookup.in b/tests/ide/emacs/InfoTable.lookup.in
similarity index 100%
rename from tests/ide/emacs/infotable.lookup.in
rename to tests/ide/emacs/InfoTable.lookup.in
diff --git a/tests/ide/emacs/infotable.lookup.out.expected b/tests/ide/emacs/InfoTable.lookup.out.expected
similarity index 100%
rename from tests/ide/emacs/infotable.lookup.out.expected
rename to tests/ide/emacs/InfoTable.lookup.out.expected
diff --git a/tests/ide/emacs/integration.fst b/tests/ide/emacs/Integration.fst
similarity index 100%
rename from tests/ide/emacs/integration.fst
rename to tests/ide/emacs/Integration.fst
diff --git a/tests/ide/emacs/integration.push-pop.in b/tests/ide/emacs/Integration.push-pop.in
similarity index 100%
rename from tests/ide/emacs/integration.push-pop.in
rename to tests/ide/emacs/Integration.push-pop.in
diff --git a/tests/ide/emacs/integration.push-pop.out.expected b/tests/ide/emacs/Integration.push-pop.out.expected
similarity index 100%
rename from tests/ide/emacs/integration.push-pop.out.expected
rename to tests/ide/emacs/Integration.push-pop.out.expected
diff --git a/tests/ide/emacs/minimal.autocomplete-global.in b/tests/ide/emacs/Minimal.autocomplete-global.in
similarity index 100%
rename from tests/ide/emacs/minimal.autocomplete-global.in
rename to tests/ide/emacs/Minimal.autocomplete-global.in
diff --git a/tests/ide/emacs/minimal.autocomplete-global.out.expected b/tests/ide/emacs/Minimal.autocomplete-global.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.autocomplete-global.out.expected
rename to tests/ide/emacs/Minimal.autocomplete-global.out.expected
diff --git a/tests/ide/emacs/minimal.autocomplete-local.in b/tests/ide/emacs/Minimal.autocomplete-local.in
similarity index 100%
rename from tests/ide/emacs/minimal.autocomplete-local.in
rename to tests/ide/emacs/Minimal.autocomplete-local.in
diff --git a/tests/ide/emacs/minimal.autocomplete-local.out.expected b/tests/ide/emacs/Minimal.autocomplete-local.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.autocomplete-local.out.expected
rename to tests/ide/emacs/Minimal.autocomplete-local.out.expected
diff --git a/tests/ide/emacs/minimal.compute.in b/tests/ide/emacs/Minimal.compute.in
similarity index 100%
rename from tests/ide/emacs/minimal.compute.in
rename to tests/ide/emacs/Minimal.compute.in
diff --git a/tests/ide/emacs/minimal.compute.out.expected b/tests/ide/emacs/Minimal.compute.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.compute.out.expected
rename to tests/ide/emacs/Minimal.compute.out.expected
diff --git a/tests/ide/emacs/minimal.describe-repl.in b/tests/ide/emacs/Minimal.describe-repl.in
similarity index 100%
rename from tests/ide/emacs/minimal.describe-repl.in
rename to tests/ide/emacs/Minimal.describe-repl.in
diff --git a/tests/ide/emacs/minimal.describe-repl.out.expected b/tests/ide/emacs/Minimal.describe-repl.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.describe-repl.out.expected
rename to tests/ide/emacs/Minimal.describe-repl.out.expected
diff --git a/tests/ide/emacs/minimal.fst b/tests/ide/emacs/Minimal.fst
similarity index 100%
rename from tests/ide/emacs/minimal.fst
rename to tests/ide/emacs/Minimal.fst
diff --git a/tests/ide/emacs/minimal.push-no-extra-info.in b/tests/ide/emacs/Minimal.push-no-extra-info.in
similarity index 100%
rename from tests/ide/emacs/minimal.push-no-extra-info.in
rename to tests/ide/emacs/Minimal.push-no-extra-info.in
diff --git a/tests/ide/emacs/minimal.push-no-extra-info.out.expected b/tests/ide/emacs/Minimal.push-no-extra-info.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.push-no-extra-info.out.expected
rename to tests/ide/emacs/Minimal.push-no-extra-info.out.expected
diff --git a/tests/ide/emacs/minimal.push-pop.in b/tests/ide/emacs/Minimal.push-pop.in
similarity index 100%
rename from tests/ide/emacs/minimal.push-pop.in
rename to tests/ide/emacs/Minimal.push-pop.in
diff --git a/tests/ide/emacs/minimal.push-pop.out.expected b/tests/ide/emacs/Minimal.push-pop.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.push-pop.out.expected
rename to tests/ide/emacs/Minimal.push-pop.out.expected
diff --git a/tests/ide/emacs/minimal.push-positional-location.in b/tests/ide/emacs/Minimal.push-positional-location.in
similarity index 100%
rename from tests/ide/emacs/minimal.push-positional-location.in
rename to tests/ide/emacs/Minimal.push-positional-location.in
diff --git a/tests/ide/emacs/minimal.push-positional-location.out.expected b/tests/ide/emacs/Minimal.push-positional-location.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.push-positional-location.out.expected
rename to tests/ide/emacs/Minimal.push-positional-location.out.expected
diff --git a/tests/ide/emacs/minimal.push.in b/tests/ide/emacs/Minimal.push.in
similarity index 100%
rename from tests/ide/emacs/minimal.push.in
rename to tests/ide/emacs/Minimal.push.in
diff --git a/tests/ide/emacs/minimal.push.out.expected b/tests/ide/emacs/Minimal.push.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.push.out.expected
rename to tests/ide/emacs/Minimal.push.out.expected
diff --git a/tests/ide/emacs/minimal.unset-current-module.in b/tests/ide/emacs/Minimal.unset-current-module.in
similarity index 100%
rename from tests/ide/emacs/minimal.unset-current-module.in
rename to tests/ide/emacs/Minimal.unset-current-module.in
diff --git a/tests/ide/emacs/minimal.unset-current-module.out.expected b/tests/ide/emacs/Minimal.unset-current-module.out.expected
similarity index 100%
rename from tests/ide/emacs/minimal.unset-current-module.out.expected
rename to tests/ide/emacs/Minimal.unset-current-module.out.expected
diff --git a/tests/ide/emacs/number.fst b/tests/ide/emacs/Number.fst
similarity index 100%
rename from tests/ide/emacs/number.fst
rename to tests/ide/emacs/Number.fst
diff --git a/tests/ide/emacs/number.fsti b/tests/ide/emacs/Number.fsti
similarity index 100%
rename from tests/ide/emacs/number.fsti
rename to tests/ide/emacs/Number.fsti
diff --git a/tests/ide/emacs/number.interface-violation-and-fix.in b/tests/ide/emacs/Number.interface-violation-and-fix.in
similarity index 94%
rename from tests/ide/emacs/number.interface-violation-and-fix.in
rename to tests/ide/emacs/Number.interface-violation-and-fix.in
index 43584044e33..70b111ccee8 100644
--- a/tests/ide/emacs/number.interface-violation-and-fix.in
+++ b/tests/ide/emacs/Number.interface-violation-and-fix.in
@@ -4,4 +4,4 @@
 {"query-id":"4","query":"pop","args":{}}
 {"query-id":"5","query":"vfs-add","args":{"filename":"number.fsti","contents":"module Number\n\nval a : a:int{a < 0}\n"}}
 {"query-id":"6","query":"push","args":{"kind":"full","code":"module Number\n","line":1,"column":0}}
-{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = -1\n","line":2,"column":0}}
+{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = 1\n","line":2,"column":0}}
diff --git a/tests/ide/emacs/number.interface-violation-and-fix.out.expected b/tests/ide/emacs/Number.interface-violation-and-fix.out.expected
similarity index 87%
rename from tests/ide/emacs/number.interface-violation-and-fix.out.expected
rename to tests/ide/emacs/Number.interface-violation-and-fix.out.expected
index e2823b698d2..6d74974576f 100644
--- a/tests/ide/emacs/number.interface-violation-and-fix.out.expected
+++ b/tests/ide/emacs/Number.interface-violation-and-fix.out.expected
@@ -1,7 +1,7 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": null, "status": "success"}
 {"kind": "response", "query-id": "2", "response": [], "status": "success"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": null, "status": "success"}
 {"kind": "response", "query-id": "5", "response": null, "status": "success"}
 {"kind": "response", "query-id": "6", "response": [], "status": "success"}
diff --git a/tests/ide/emacs/number.interface-violation.in b/tests/ide/emacs/Number.interface-violation.in
similarity index 100%
rename from tests/ide/emacs/number.interface-violation.in
rename to tests/ide/emacs/Number.interface-violation.in
diff --git a/tests/ide/emacs/number.interface-violation.out.expected b/tests/ide/emacs/Number.interface-violation.out.expected
similarity index 81%
rename from tests/ide/emacs/number.interface-violation.out.expected
rename to tests/ide/emacs/Number.interface-violation.out.expected
index 59c46faba85..1f5309d9a3b 100644
--- a/tests/ide/emacs/number.interface-violation.out.expected
+++ b/tests/ide/emacs/Number.interface-violation.out.expected
@@ -1,4 +1,4 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": null, "status": "success"}
 {"kind": "response", "query-id": "2", "response": [], "status": "success"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"}
diff --git a/tests/ide/emacs/search.cons-snoc.in b/tests/ide/emacs/Search.cons-snoc.in
similarity index 100%
rename from tests/ide/emacs/search.cons-snoc.in
rename to tests/ide/emacs/Search.cons-snoc.in
diff --git a/tests/ide/emacs/search.cons-snoc.out.expected b/tests/ide/emacs/Search.cons-snoc.out.expected
similarity index 100%
rename from tests/ide/emacs/search.cons-snoc.out.expected
rename to tests/ide/emacs/Search.cons-snoc.out.expected
diff --git a/tests/ide/emacs/search.fst b/tests/ide/emacs/Search.fst
similarity index 100%
rename from tests/ide/emacs/search.fst
rename to tests/ide/emacs/Search.fst
diff --git a/tests/ide/emacs/test.fst b/tests/ide/emacs/Test.fst
similarity index 100%
rename from tests/ide/emacs/test.fst
rename to tests/ide/emacs/Test.fst
diff --git a/tests/ide/emacs/test.fsti b/tests/ide/emacs/Test.fsti
similarity index 100%
rename from tests/ide/emacs/test.fsti
rename to tests/ide/emacs/Test.fsti
diff --git a/tests/ide/emacs/tutorial.fst b/tests/ide/emacs/Tutorial.fst
similarity index 100%
rename from tests/ide/emacs/tutorial.fst
rename to tests/ide/emacs/Tutorial.fst
diff --git a/tests/ide/emacs/tutorial.push.in b/tests/ide/emacs/Tutorial.push.in
similarity index 100%
rename from tests/ide/emacs/tutorial.push.in
rename to tests/ide/emacs/Tutorial.push.in
diff --git a/tests/ide/emacs/tutorial.push.out.expected b/tests/ide/emacs/Tutorial.push.out.expected
similarity index 100%
rename from tests/ide/emacs/tutorial.push.out.expected
rename to tests/ide/emacs/Tutorial.push.out.expected
diff --git a/tests/ide/emacs/tutorial.segment.in b/tests/ide/emacs/Tutorial.segment.in
similarity index 100%
rename from tests/ide/emacs/tutorial.segment.in
rename to tests/ide/emacs/Tutorial.segment.in
diff --git a/tests/ide/emacs/tutorial.segment.out.expected b/tests/ide/emacs/Tutorial.segment.out.expected
similarity index 100%
rename from tests/ide/emacs/tutorial.segment.out.expected
rename to tests/ide/emacs/Tutorial.segment.out.expected
diff --git a/tests/micro-benchmarks/arith.fst b/tests/micro-benchmarks/Arith.fst
similarity index 100%
rename from tests/micro-benchmarks/arith.fst
rename to tests/micro-benchmarks/Arith.fst
diff --git a/tests/micro-benchmarks/arith.fst.hints b/tests/micro-benchmarks/Arith.fst.hints
similarity index 100%
rename from tests/micro-benchmarks/arith.fst.hints
rename to tests/micro-benchmarks/Arith.fst.hints
diff --git a/tests/micro-benchmarks/Mac.fst b/tests/micro-benchmarks/MAC.fst
similarity index 100%
rename from tests/micro-benchmarks/Mac.fst
rename to tests/micro-benchmarks/MAC.fst
diff --git a/tests/micro-benchmarks/Mac.fst.hints b/tests/micro-benchmarks/MAC.fst.hints
similarity index 100%
rename from tests/micro-benchmarks/Mac.fst.hints
rename to tests/micro-benchmarks/MAC.fst.hints