Hurkens.v: update comments.
Remove some 'deprecated' warnings.
Improve consistency of whitespace (beautifier).
Add several reproduction files for bugs.
Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",
as "||" is actually redefined in "plugins/micromega/sos_lib.ml".
Fix incorrect assert false in detyping.
Test cases for closed bugs.
Adding a test for bug #3653.
Bug #3566 is fixed.
Add missing "Fail" to bug cases.
Add a bunch of reproduction files for bugs.
Hurkens.v: fix coqdoc formatting in a comment.
Hurkens.v: new paradox: type of modal propositions is not a retract.

In particular there is no retract of the type of negative propositions in a negative proposition.
ClassicalFacts: adds a proof that weak excluded middle implies weak proof irrelevance.

Application of previous commit in Hurkens.v.