Better error messages

src/CFlatToWasm.ml

@@ -39,7 +39,7 @@ let find_global env name =
   try
     StringMap.find name env.globals
   with Not_found ->
-    Warnings.fatal_error "Could not resolve global %s" name
+    Warnings.fatal_error "Could not resolve global %s (look out for Warning 12)" name
 
 (* Some functions were marked as assumed in F*, and then implemented by hand in
  * C. But, now, we have to re-implement them in F* so that they get Wasm codegen

src/Kremlin.ml

@@ -95,7 +95,7 @@ The default is %s and the available warnings are:
   7: private F* function cannot be marked as C static
   8: C inline function reference across translation units
   9: need to manually call static initializers for globals
-  10: dropping a polymorphic function definition
+  10: <currently unused>
   11: subexpression is not Low*; cannot proceed
   12: cannot be compiled to Wasm
 

src/Warnings.ml

@@ -18,7 +18,6 @@ and raw_error =
   | LostStatic of string option * lident * string option * lident
   | LostInline of string option * lident * string option * lident
   | MustCallKrmlInit
-  | NoPolymorphism of lident
   | NotLowStar of expr
   | NotWasmCompatible of lident * string
 
@@ -81,8 +80,6 @@ let errno_of_error = function
       8
   | MustCallKrmlInit ->
       9
-  | NoPolymorphism _ ->
-      10
   | NotLowStar _ ->
       11
   | NotWasmCompatible _ ->
@@ -135,10 +132,6 @@ let rec perr buf (loc, raw_error) =
         before starting main(). You did not provide a main function, so users of \
         your library MUST MAKE SURE they call kremlinit_globals(); (see \
         kremlinit.c)"
-  | NoPolymorphism lid ->
-      p "%a is polymorphic and must be either marked as noextract or, \
-        alternatively, as [@\"substitute\"] in the hope \
-        that, once expanded at call-site, it type-checks as Low*" plid lid
   | NotLowStar e ->
       p "this expression is not Low*; the enclosing function cannot be translated into C*: %a" pexpr e
   | NotWasmCompatible (lid, reason) ->