matita.cs.unibo.it Git - helm.git/search

]> matita.cs.unibo.it Git - helm.git/search

2010-09-30	Claudio Sacerdoti...	Stuff moved from old Matita.	commit \| commitdiff \| tree
2010-09-30	Claudio Sacerdoti...	Towards Matita 1.0 (new kernel etc. only).	commit \| commitdiff \| tree
2010-07-29	Claudio Sacerdoti...	Bug fixed: nodes were copied.	commit \| commitdiff \| tree
2010-07-28	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-07-23	Claudio Sacerdoti...	Some experiments on a co-inductive Heityng algebra.	commit \| commitdiff \| tree
2010-07-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-07-04	Claudio Sacerdoti...	Some important proofs/definitions were (and are still...	commit \| commitdiff \| tree
2010-07-01	Claudio Sacerdoti...	Proof simplified.	commit \| commitdiff \| tree
2010-07-01	Claudio Sacerdoti...	Proof simplified (??).	commit \| commitdiff \| tree
2010-05-06	Claudio Sacerdoti...	Bug fixed: nstatus => status (to undo the changes).	commit \| commitdiff \| tree
2010-05-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-05-06	Claudio Sacerdoti...	assert false could happen	commit \| commitdiff \| tree
2010-05-06	Claudio Sacerdoti...	Bug fixed:	commit \| commitdiff \| tree
2010-05-05	Claudio Sacerdoti...	coinduction is between us	commit \| commitdiff \| tree
2010-05-05	Claudio Sacerdoti...	First tests.	commit \| commitdiff \| tree
2010-05-04	Claudio Sacerdoti...	Regular expressions.	commit \| commitdiff \| tree
2010-04-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-04-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-04-14	Claudio Sacerdoti...	Formal points.	commit \| commitdiff \| tree
2010-04-14	Claudio Sacerdoti...	Some dualization clean-up.	commit \| commitdiff \| tree
2010-04-08	Claudio Sacerdoti...	New code (unbranched) to compute all keys by all possible...	commit \| commitdiff \| tree
2010-04-08	Claudio Sacerdoti...	New sets of.	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	Not is now inductive.	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	Use the inversion!	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	Bug fixed: the current equation is not always the last...	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	- inversion principles are now generated also for co...	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	More debugging info from print_tac.	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	Implicit and UserInput were printed incorrectly.	commit \| commitdiff \| tree
2010-03-31	Claudio Sacerdoti...	ninversion	commit \| commitdiff \| tree
2010-03-26	Claudio Sacerdoti...	Good definition found.	commit \| commitdiff \| tree
2010-03-26	Claudio Sacerdoti...	(Co)Inductively Generated Formal Topologies (not only...	commit \| commitdiff \| tree
2010-03-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Nice examples for automation (that fails).	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Simplified proof after pattern fix	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	"Not" is no longer a definition	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	The precedence of ^-1 has changed.	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Equality has one right parameter and thus it's elimination...	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-03-24	Claudio Sacerdoti...	Real numbers as co-inductive streams of digits (overlapping...	commit \| commitdiff \| tree
2010-03-18	Claudio Sacerdoti...	Do not index examples (concrete syntax: nremark).	commit \| commitdiff \| tree
2010-03-18	Claudio Sacerdoti...	nremark => `Example (not to be indexed)	commit \| commitdiff \| tree
2010-03-17	Claudio Sacerdoti...	OCaml's inferred type simplified.	commit \| commitdiff \| tree
2010-03-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-03-16	Claudio Sacerdoti...	Comparison of two applications with a different number...	commit \| commitdiff \| tree
2010-03-16	Claudio Sacerdoti...	1) intros cleans up the cache (because the context...	commit \| commitdiff \| tree
2010-03-16	Claudio Sacerdoti...	refreshing of inferred type was missing	commit \| commitdiff \| tree
2010-03-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-02-15	Claudio Sacerdoti...	The height of fixpoint applications was not computed...	commit \| commitdiff \| tree
2010-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	End of curryfication of binary_morphisms.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Curryfication of binary_morphisms.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Curryfication of binary setoids.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Curryfication of binary morphisms.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Work in Progress: Who needs binary_morphisms? Curryfication...	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Debug code commented out.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Parts of the status were not re-initialized correctly...	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Bad variable name fixed.	commit \| commitdiff \| tree
2010-02-03	Claudio Sacerdoti...	Bug fixed: projection redexes obtained reducing other...	commit \| commitdiff \| tree
2010-01-19	Claudio Sacerdoti...	We can always use the "covered by emptyset" relation...	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	More //.	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	More // everywhere.	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	// used everywhere!	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	// in place of nauto everywhere	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	// is now more powerful	commit \| commitdiff \| tree
2010-01-18	Claudio Sacerdoti...	// is now more powerful	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	A slightly more complicated example.	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	Finished!	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	We are still equivalent (even if the definition of...	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	Urrah!	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	Extending to the nAx set.	commit \| commitdiff \| tree
2010-01-15	Claudio Sacerdoti...	Skipfact function (a partial general recursive function...	commit \| commitdiff \| tree
2010-01-11	Claudio Sacerdoti...	Finished	commit \| commitdiff \| tree
2010-01-08	Claudio Sacerdoti...	Improved	commit \| commitdiff \| tree
2010-01-08	Claudio Sacerdoti...	Partial porting to new syntax.	commit \| commitdiff \| tree
2010-01-08	Claudio Sacerdoti...	Source language path must be appended, not replaced.	commit \| commitdiff \| tree
2010-01-08	Claudio Sacerdoti...	Categorical stuff postponed.	commit \| commitdiff \| tree
2010-01-06	Claudio Sacerdoti...	Simplified.	commit \| commitdiff \| tree
2010-01-06	Claudio Sacerdoti...	Coercions via unification hints?	commit \| commitdiff \| tree
2010-01-02	Claudio Sacerdoti...	1) stuff moved from categories.ma to setoids*.ma	commit \| commitdiff \| tree
2009-12-30	Claudio Sacerdoti...	Almost done (up to definition of category).	commit \| commitdiff \| tree
2009-12-30	Claudio Sacerdoti...	Porting of Sambin's stuff started.	commit \| commitdiff \| tree
2009-12-30	Claudio Sacerdoti...	Porting of Sambin's stuff started.	commit \| commitdiff \| tree
2009-12-30	Claudio Sacerdoti...	Removed line is back again.	commit \| commitdiff \| tree
2009-12-30	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-11-12	Claudio Sacerdoti...	Code made more uniform.	commit \| commitdiff \| tree
2009-11-04	Claudio Sacerdoti...	Bug fixed: restrict used to take the list of positions...	commit \| commitdiff \| tree
2009-11-04	Claudio Sacerdoti...	1) sort computation undone (it used to be bugged anyway)	commit \| commitdiff \| tree
2009-10-30	Claudio Sacerdoti...	Code simplified.	commit \| commitdiff \| tree
2009-10-30	Claudio Sacerdoti...	Useless old code for ad-hoc management of out-scope...	commit \| commitdiff \| tree
2009-10-30	Claudio Sacerdoti...	New style debugging/profiling for NCicMetaSubst.	commit \| commitdiff \| tree
2009-10-30	Claudio Sacerdoti...	Sometimes it is useful to be able to print the subst...	commit \| commitdiff \| tree
2009-10-29	Claudio Sacerdoti...	Better error message.	commit \| commitdiff \| tree
2009-10-29	Claudio Sacerdoti...	For some obscure reason, more universes are now needed...	commit \| commitdiff \| tree
2009-10-29	Claudio Sacerdoti...	instantiate/sortfy/kindfy etc. reimplemented with less...	commit \| commitdiff \| tree
2009-10-29	Claudio Sacerdoti...	New function.	commit \| commitdiff \| tree
next

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom