From: Ferruccio Guidi Date: Wed, 21 Feb 2007 14:15:55 +0000 (+0000) Subject: procedural : some improvements. X-Git-Tag: 0.4.95@7852~587 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f38b6dc5e48855b7a2170de5a5ccb30aded766c;hp=3f38b6dc5e48855b7a2170de5a5ccb30aded766c;p=helm.git procedural : some improvements. decompose tactic: user provided premise and types removed. The decomposable types are now the non-recursive inductive types without right parameters and are auto-detected ---