Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • 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
  • IrisIris
  • Merge requests
  • !386

no longer reftest old Coq 8.9

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Ralf Jung requested to merge ralf/reftest into master Feb 28, 2020
  • Overview 1
  • Commits 1
  • Pipelines 0
  • Changes 13

This adds Coq 8.9 to the Coq versions for which we do not expect tests to produce the right output. That lets us remove the annoying ltac backtraces.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/reftest