Less ambitious application of a notation for eq_rect. We proposed

"rewrite Heq in H" but "rewrite" is sometimes used by users and I
don't want to have to change their file.

The solution to put the notations in a module does not work with name
"rewrite" because loading the module would change the status of
"rewrite" from simple ident to keyword (and we cannot declare
"rewrite" as an ident, as shown in previous commit).

Then we come back on notation "rew" (this name is also used by some
users), in a module.

This continues commit r14366 and r14390 and improves on the level of
the notation.

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

0 files changed, 0 insertions, 0 deletions