Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 16
    • Merge requests 16
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !148

Create HintDBs with the discriminated option

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Michael Sammler requested to merge msammler/hintdb_discriminated into master Apr 20, 2020
  • Overview 12
  • Commits 1
  • Pipelines 0
  • Changes 2

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.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: msammler/hintdb_discriminated