Skip to content

Create HintDBs with the discriminated option

Michael Sammler requested to merge msammler/hintdb_discriminated into master

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.

Merge request reports