Changes to declarative tactics, implementation of equality chain

Changes to declarative tactics, implementation of equality chain

Fix type for RewritingStep, add a type for Print Stack (a debug tool)

Fix PP for RewritingStep, generalized just_to_tactic_just for the type
[>`Auto of auto_params | `Term of NotationPt.term]

Add parsing rule for print_stack, fix parsing rules for obtain, conclude
e =

Fix indentation for declarative.ml

Change mk_just to return a tactic (instead of a lowtactic)

Modify extract_first_goal_from_status to take the first goal from the
stack, instead of the metasenv

Change assume, suppose, andelim and existselim to use distribute_tac

Add a mustdot function to check whether there's the need to call the
dot_tactic at the end. The dot tactic is used to focus on a single goal
at the time when there are multiple open goals

Change bydone to use the dot tactic to switch between multiple goals

Modify we_need_to_prove to use the dot_tac to focus on a single goal

Add a type_of_tactic_term function to extract the type of a tactic_term
(used in RewritingStep)

Implement rewritingstep, which covers conclude and =; obtain is in the
works

Implement print_stack, for debug purposes (prints the stack to stderr)

Modify declarative's signature to add the new functions

Add firs_tac to nTactic's signature

Change auto_lowtac's signature to return a tactic

Correct natural_deduction.ma for the new version. Had to change some
\forall with \Pi