Fix typo in cf04daec997.
Clean outdated comment in Proofview.Notations.
Remove spurious [1] in equality.ml.

Introduced in a4043608f
Untyped terms in ltac: simplify [coerce_to_uconstr].

Following advice by Hugo Herbelin.
Add primtive [num_goal] to Proofview.

The [num_goal] tactic counts the number of focused goals.
Add [numgoal] to Ltac.
Add [guard] tactic.

The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails.

Together with [numgoal] can be used to fork on the number of goals of a tactic.

The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
Document [numgoals] and [guard].
CHANGES: [numgoals] and [guard].
Fix English spelling -> American spelling in doc.
New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.

Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.

In other words t;[t1…tn] is [> t;[>t1…tn].. ].
Document [> … ].
CHANGES: [>…].
Faster uconstr.

Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.