X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.txt;h=378fa5a4bdcd6f223544b5fc419e8de03c7a8385;hb=bbdf43ea2ac586be4f3c0779e98642b8f7bd1a03;hp=ce34e404ca1dabdbf5aefaaa24388340d78fb026;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git
diff --git a/helm/software/matita/matita.txt b/helm/software/matita/matita.txt
index ce34e404c..378fa5a4b 100644
--- a/helm/software/matita/matita.txt
+++ b/helm/software/matita/matita.txt
@@ -1,3 +1,35 @@
+###
+ Regole di eliminazione per tipi induttivi:
+ > - as you point it out, unit implies small, hence the clause "if
+ > Environ.engagement ..." is useles; revision 1.46 apparently missed
+ > this point;
+ and I was wrong. Components of constructors that are arities in Prop
+ (i.e. of the form ... -> Prop) are considered as unit (at least in
+ Coq). Hence you can have non small unit types. The typical example is
+
+ Inductive T : Prop := C : Prop -> T.
+
+ As a consequence, my modification of the code of Indtypes.allowed_sorts
+ introduced a consistency hole (with elimination from T to Type, Prop
+ becomes equivalent to T and system Type:Type becomes a subsystem of
+ Coq). If you have a similar allowance in Matita, it may be problematic
+ too.
+
+
+
+** introdurre una tattica primitiva "enlarge_metasenv" che cambia il metasenv
+ aggiungendo nuove meta e tenendo traccia dei nuovi goal aperti; usarla
+ ovunque rimuovendo ProofEngineHelpers.compare_metasenv. Questo dovrebbe
+ anche permettere a lungo termine di rendere lo stato un tipo opaco.
+
+
+Possibile causa di rallentamenti:
+1. The last commit that fixed unification of compound coercions with
+ applied atomic coercions used to introduce too many compound coercions
+ at the end. In this commit we fix the problem in a brutal way by
+ mergin coercions every time CicMetaSubst.apply_subst is called.
+ To be refined later on.
+
Ferruccio ha cambiato matita.lang:
> iforall
> iexists
@@ -37,7 +69,6 @@ TODO
- tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire
- comportamento di tutte le tattiche nei confronti dei let-in
- elim con pattern
- - assiomi (manca sintassi concreta e AST).
- Dare errore significativo al posto di NotWellTypedInterpreation -> CSC
- elim_intros_simpl e rewrite_simpl: ora non viene usata dal
^^^^^^ ^^^^^^
@@ -113,9 +144,10 @@ TODO
- non chiudere transitivamente i moo ??
DEMONI E ALTRO
- - compilare Whelp
DONE
+- compilare Whelp -> Gares, Zack, CSC
+- assiomi (manca sintassi concreta e AST) -> CSC
- in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e
eval_from_stream_greedy -> CSC
- menu contestuale (tasto dx) nel sequent viewer -> Zack