master branch is broken

Stream: general

[Scott Morrison]

Ugh, master is broken in mathlib.

[Scott Morrison]

arguta:mathlib scott$ git status
On branch master
Your branch is up-to-date with 'origin/master'.

nothing to commit, working tree clean
arguta:mathlib scott$ lean --make tests/tactics.lean
/Users/scott/projects/lean/mathlib/tests/tactics.lean:641:2: error: is_def_eq tactic failed, the following expressions are not definitionally equal (remark: is_def_eq tactic does modify the metavariable assignment)
  p : Prop
and
  s : Prop
state:
p q r s : Prop,
h₀ : p ↔ q,
h₁ : q ↔ r,
h₂ : r ↔ s
⊢ p ↔ s

[Scott Morrison]

(I spent 20 minutes trying to work out how my branch had broken something, before realising it wasn't my fault.)

[Simon Hudon]

My bad. we should comment out those tests while I'm fixing that tactic

[Simon Hudon]

@Mario Carneiro Can you comment out these test cases please?

[Mario Carneiro]

eh, can you PR it? It takes me an hour to move to and from module branch

[Simon Hudon]

Here you go: https://github.com/leanprover/mathlib/pull/398