Prettyp: avoid useless "let module"

 As hinted by X. Clerc, a "let module" induces some runtime cost,
 so let's try to avoid them when possible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes

 This file, which is currently expected to fail at the last line
 (with Universe Inconsistency), was actually failing earlier
 after Pierre Boutillier changed the patterns (parameters are required now).

 A final "Fail" will soon arrives here to avoid such issue in the future...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
Uminus.v : prepare this test file for the use of Fail

 - Highlight the fact that the line defining "up" is the one which
   should fail.
 - Factor code with stdlib's Hurkens.v
 - This way, this test could become a "shouldnotfail" test by placing
   two final "Fail" (before the definitions of "up" and "paradox").

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