Fixing Equality.injectable which did not detect an equality without

constructors as non relevant for injection. Also made injection
failing in such situation.

Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases
(observed in the compilation of CoinductiveReals.LNP_Digit). The
most probable explanation is that this loop was formerly protected by
a failing rewrite which stopped failing after revision 14549 made
second-order pattern-matching more powerful.

Also suppressed dead code in Invfun.intros_with_rewrite.

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

0 files changed, 0 insertions, 0 deletions