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
Ready to merge by members who can write to the target branch.

Merge details

  • 4 commits and 1 merge commit will be added to .
  • Source branch will not be deleted.

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