Added strings to prelude to fix printing of strings.length

This should hopefully fix strings.length showing up in random places. I tested it with iris and RefinedC. Both compile without changes and length is no more printed as strings.length in RefinedC. See the comment for the reasoning why I think this works.

theories/prelude.v

@@ -10,4 +10,13 @@ From stdpp Require Export
   fin_sets
   listset
   list
+  (* This must be exported after base (which exports Coq.List) since
+  it exports the length notation to ensure that we use List.length and
+  not Strings.length. If we don't export strings here and some file
+  imports strings and then the prelude (which seems to happen with
+  Iris), the definition in Coq.List will shadow the notation in
+  stdpp.strings and length will be printed as strings.length since Coq
+  prefers printing the notation (strings.length) instead of the
+  definition which shadows it. *)
+  strings
   lexico.

[Robbert Krebbers]

This = strings?

[Ralf Jung]

Wouldn't it make more sense for Iris to import the prelude first?

[Michael Sammler]

I don't know where strings gets imported in Iris. It can also be that something in iris exports the prelude, then strings and then the prelude again (this can easily happen because many files in iris export the prelude since it it exported transitively).

[Robbert Krebbers]

algebra/base.v exports prelude.

There are a bunch of spurious exports of std.strings here and there, but probably all of those can be removed:

$ mgrep std.*string
theories/proofmode/sel_patterns.v:From stdpp Require Export strings.
theories/proofmode/intro_patterns.v:From stdpp Require Export strings.
theories/proofmode/spec_patterns.v:From stdpp Require Export strings.
theories/proofmode/notation.v:From stdpp Require Export strings.
theories/proofmode/base.v:From stdpp Require Export strings.
theories/heap_lang/lang.v:From stdpp Require Export binders strings.