A tentative uniform naming policy in module Inductiveops.

- realargs: refers either to the indices of an inductive, or to the proper args
  of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs

- realdecls: refers to the defining context of indices or proper args
  of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
Continuing (incomplete) cleaning of Inductiveops.
micromega : improve efficiency/termination of type-checking

* unused terms are generalised
* proof is abstract
Compatibility for compilation with ocaml 3.12 (at least).
micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)

* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
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.