Create HintDBs with the discriminated option
According to the documentation https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb, when creating a hint database without discrimination, Coq uses the legacy implementation, which only uses Discrimination Trees for goals without evars and does not use opaqueness information. This commit switches the hint databases of stdpp to the new implementation.