Many changes

Many changes

Add a BetaRewritingStep tactic, for multiple 'or equivalently'
statements in theorems proofs

Remove old code

Add a key-value list to the tiny-cals stack (parameters list) for
context related infos. Can be used as a general purpose store for
key-value pairs

Adapt code that works on the stack to work with the new parameter list

Add function to add and retrieve key-value pairs to the parameters list

Add the concept of volatile-context: they are contexts that are cleared
after the application of some tactics. E.g., the context for a
beta_rewriting (sequence of 'or equivalently') is a volatile context, as
any tactic breaks the chain

Add a function to clear volatile parameters from the paramters list

Add a case in extract_first_goal_from_status for the case where the
stack is empty

Make the tactics that make use of distribute High tactics

Reimplement the dot tac on top of the stack to handle branching. This
makes use of the second iterator list of the stack

Add a "done_continuation" function that checks whether it needs to dot
or recursively merge branches after a done statement

Add a function to push goals from the focus iterator list of the
previous level on the stack to the second iteretaor list of the current
level

Change conclude and obtain to use a volatile context to obligate the
user to only use = inside it

Change the add_names_to_goals function to use the stack instead of the
metasenv directly

Add a unfocus_branch_tac to unfocus from goals in a stack level (useful
for cases and induction)

Change induction and cases to use a context to obligate the user to use
case only inside it. Furthermore, the new stack based branching for
declarative tactics obligates the user to only switch between cases of
the last level

Change induction and cases to start without focusing on any goal and
without automatically focusing on the next goal after a done. The user
is compelled to use case to switch between each case

Change the case to only change case when the current case has been dealt
with

Attempt to fix automation

Add first draft for matita's helper