New tactic to rewrite decidability lemmas when one knows which side

is true. E.g. "decide (eq_nat_dec n 0) with H" on

  H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1

returns

  H: n=0 |- 1 = 1 .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions