From: Andrea Berlingieri <andrea.berlingieri@studio.unibo.it>
Date: Sun, 12 May 2019 15:19:18 +0000 (+0200)
Subject: Add support for proving cases in a different order
X-Git-Tag: make_still_working~229^2~1^2~1^2~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=90e823f96159811d88b275df9c3ec9a4c40ff816;hp=90e823f96159811d88b275df9c3ec9a4c40ff816;p=helm.git

Add support for proving cases in a different order

Add some debug pretty printing methods and tactics.

Add a tactic to add names to metasenv goals from a given constructor
list

Modify "we_proceed_by_induction_on" to gather info on the inductive type of
the term being eliminated, apply the right constructor to the right
number of Implicit arguments, and name the new open goals

Modify "we_proceed_by_cases_on" in an analogous way to
"we_proceed_by_induction_on"

Add a tactic to focus on a given case, if present, with helper functions
for it

Modify case to search for the given case and focus on it

Modify indtyinfo to memorize also the costructor list of the inductive
type

Remove a useless if-then-else in index_local_equations2

Remove some old code, comments and trailing spaces
---