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

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

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
2009-10-29	Claudio Sacerdoti...	Let's use already existent functions.	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	Works again	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	Ad-hoc management of ? vs out_scope in instantiate...	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	Bug fixed: the `IsTerm attribute is now added by mk_meta...	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	1) new-style debugging/profiling code for old reduction	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	Commented out code to optimize the case t1 vs t2 when...	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	One-shot aliases were no longer generated because of...	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	Different aliases, better equality inferred.	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	instances	commit \| commitdiff \| tree
2009-10-28	Claudio Sacerdoti...	instance fixed	commit \| commitdiff \| tree
2009-10-26	Claudio Sacerdoti...	qed => nqed.	commit \| commitdiff \| tree
2009-10-26	Claudio Sacerdoti...	Now the time required to eval a command is printed.	commit \| commitdiff \| tree
2009-10-23	Claudio Sacerdoti...	Alias required now ??	commit \| commitdiff \| tree
2009-10-21	Claudio Sacerdoti...	Non general recursion implemented via recursion over...	commit \| commitdiff \| tree
2009-10-20	Claudio Sacerdoti...	- Bug fixed: some assert failure were just failures...	commit \| commitdiff \| tree
2009-10-19	Claudio Sacerdoti...	Smarter implementation of instantiate to avoid re-checking...	commit \| commitdiff \| tree
2009-10-15	Claudio Sacerdoti...	Profiling code integrated.	commit \| commitdiff \| tree
2009-10-14	Claudio Sacerdoti...	Debugging improved.	commit \| commitdiff \| tree
2009-10-14	Claudio Sacerdoti...	Benchmarking integrated in folding/unfolding.	commit \| commitdiff \| tree
2009-10-14	Claudio Sacerdoti...	Error message fixed (dereferencing must be done eagerly...	commit \| commitdiff \| tree
2009-10-14	Claudio Sacerdoti...	Serious bug fixed: fix_sorts used to allow inference...	commit \| commitdiff \| tree
2009-10-12	Claudio Sacerdoti...	1) Bug fixed: the case Meta(i) vs Meta(i) was handled...	commit \| commitdiff \| tree
next

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

RSS Atom