Skip to content
Snippets Groups Projects

Remove hint db and import of omega, since omega will be removed from Coq.

Merged Remove hint db and import of omega, since omega will be removed from Coq.
robbert/omega into master
Merged Robbert Krebbers requested to merge robbert/omega into master

Merge request reports

Approval is optional

Merged by Ralf JungRalf Jung 4 years ago (Jan 19, 2021 11:33am UTC)

Merge details

  • Changes merged into master with 96cb4bc9.
  • Deleted the source branch.

Pipeline #40688 passed

Stage: build

Pipeline passed for 96cb4bc9 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply