Many changes

Many changes

Change auto_params in grafiteAst.ml from being abstract on the 'term list
to being concretized to nterm list. Modify type just accordingly. Modify ntactic
types accordingly.

Add ExistsElim, AndElim, RewritingStep, Thesisbecomes types to ntactic.

Add pretty printing for ExistsElim, AndElim, RewritingStep, Thesisbecomes.

Add calls in grafite engine for the implementation of ExistsElim, AndElim, Thesisbecomes.

Add parsing rule for the "let x := t" tactic. It uses the NLetIn
ntactic.

Add parsing rules for Thesisbecomes and Rewritingstep (conclude, obtain
and =).

Modify mk_just to use the new auto_lowtac entry point for automation for
LCF-like tactics.

Remove same_type function in declarative.ml.

Add are_convertible function in declarative that uses beta-conversion.

Add a lambda_abstract tactic that abstracts the common parts of suppose
and assume. Add 3 Exception types for this tactic to handle error
situations. Modify assume and suppose accordingly

Add assert_tac that verifies that a given term is the same as the
conclusion and that two given types are beta-convertible, if a second
type is given. If all checks pass a continuation is exec'd, otherwise an
exception is raised.

Modify we_need_to_prove, by_just_we_proved to use assert_tac.

Add implementation of thesisbecomes.

Add implementation of existselim and andelim.

Modify declarative signature to add the new tactics.

Add a flag to index_local_equations and index_local_equations2 to
inhibit the use of global candidates. Modify all the functions that call
these two functions and the calls to those functions accordingly
(auto_main, do_something, top_cache, intros, auto_clusters)

Add a flag to auto_tac' to specify whether to use local candidates or
not. Modify the part where the local cands are calculated to check the
flag before proceeding.

Add auto_params to nnAuto.

Modify auto_tac to auto_tac' which takes the candidates to use
explicitly as a parameter and two flags that indicate whether to use
local candidates and whether to use only the given candidates.

Add a candidates_from_ctx function to calculate the candidates in a
given context.

Add a auto_lowtac entry point for LCF-like tactics.

Modify nnAuto signature to use auto_params instead of its explicit
version (nterm list * (string * string) list).

Add new "keywords" to matita.lang.

Add debug prints for a bug where the program would freeze. (They can
probably be removed)