I already have a
String module imported and want import
CoqsString I was thinking about something like
Require Coq.Strings.String as CoqString but obviously this is not valid
You can do
Require Coq.Strings.String. Module CoqString = Coq.Strings.String.
Oh that's it, I was trying something like
Module CoqString. Require Export Coq.Strings.String. End CoqString
Thank you Guillaume!
Last updated: Feb 06 2023 at 12:04 UTC