Dead code + typo.
Basic lemmas about the algebraic structure of equality.
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Fixing introduction patterns * and ** when used in a branch so that they do not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Use of "H"-based names for propositional hypotheses obtained by
destruction of schemes in Type such as sumbool.

Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).

This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.

Examples:

*** Non dependent case ***

Goal {True}+{False}-> True.
intros [|].

Before:

  t : True
  ============================
   True

and

  f : False
  ============================
   True

After:

  H : True
  ============================
   True

  H : False
  ============================
   True

*** Dependent case ***

Goal forall x:{True}+{False}, x=x.
intros [|].

Before:

  t : True
  ============================
   left t = left t

  f : False
  ============================
   right f = right f

After:

  HTrue : True
  ============================
   left HTrue = left HTrue

  HFalse : False
  ============================
   right HFalse = right HFalse
A little bit of documentation about V5.10 and V6.3 and V7.
Removing symmetry from the atomic tactics.
Fixing incorrect printf format.
The tactic interpreter now uses a new type of tactics, through
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.

This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
A bug has been closed (HoTT/coq #105)
cbn understand ! Arguments directive

Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
- Keep all <= constraints during refinement, otherwise we might miss collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
Fix handling of anonymous Type in template universe polymorphic inductives
to not interfere with already declared universes.
- Fix hashing of levels to get the "right" order in universe contexts etc...
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
- Force every universe level to be >= Prop, so one cannot "go under" it anymore.
- Finish the change to level-to-level substitutions, in the checker.
- Allow parsing of @const@{instance} for specifying universe instances of polymorphic
constants.
Fix canonical structure resolution (makes test-suite files go through again).
- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.