1. We only accept an algebraic type declaration

    T 'a1 ... 'aN

whenever every constructor has ls_value = Some (T 'a1 ... 'aN),
no type variable renaming is allowed.

2. We only accept an inductive predicate declaration

    P (_x1 : T1) ... (_xN : TN)

whenever every inductive clause has a conclusion of the form
(P (t1 : T1) ... (tN : TN)), no type variable renaming is allowed.

3. To this purpose, we must typecheck the whole (mutual) inductive
declaration group in the same denv. This must be ok, since user-named
type variables cannot be destructively instantiated anyway. However,
I'd like Jean-Christoph to check my changes in Typing.add_inductives.

new theories ArraySorted and ArrayPermut; new program example quicksort.mlw in progress (but triggers a bug in inductive elimination)

in the database given by -d
display only differences, --debug benchdb for other information.

simplify greatly the implementation, work less in advance.

Rebase : Use the new call_prover interface

which appear only in the type value

Currently all the variables that appear in the return value
are used as supplementarry argument.

rebuild provers-data-conf when necessary; support for Gappa 0.14.0 (but Gappa's driver still to be fixed)