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

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

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
2009-10-12	Claudio Sacerdoti...	Bug fixed: in case of (t ...) where t has flexible...	commit \| commitdiff \| tree
2009-10-12	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2009-10-12	Claudio Sacerdoti...	Closed metas must have closed (expected) types.	commit \| commitdiff \| tree
2009-10-12	Claudio Sacerdoti...	Improved debugging code.	commit \| commitdiff \| tree
2009-10-08	Claudio Sacerdoti...	A new switch to activate/deactive nCicReduction pretty...	commit \| commitdiff \| tree
2009-10-08	Claudio Sacerdoti...	Printing extremely large terms no longer raises Failure.	commit \| commitdiff \| tree
2009-10-07	Claudio Sacerdoti...	Performance improvement by preserving more sharing...	commit \| commitdiff \| tree
2009-10-07	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree
2009-10-07	Claudio Sacerdoti...	- oCic2NCic and nCic2OCic moved to ng_library	commit \| commitdiff \| tree
2009-10-06	Claudio Sacerdoti...	Improved error message.	commit \| commitdiff \| tree
2009-10-05	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-05	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-05	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	Does not compile! Wrong unification hint?	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-10-02	Claudio Sacerdoti...	Wrong context (again!)	commit \| commitdiff \| tree
2009-10-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-09-30	Claudio Sacerdoti...	With this hint, it diverges.	commit \| commitdiff \| tree
2009-09-30	Claudio Sacerdoti...	New datatype for metasenv/subst: full fledged attributes...	commit \| commitdiff \| tree
2009-09-30	Claudio Sacerdoti...	Better (but still broken) fix for the case ?sort vs...	commit \| commitdiff \| tree
2009-09-30	Claudio Sacerdoti...	The term contains dummy.conv that was searched over...	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	1) improved (???) debugging, with	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	Re-indentiation	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	The unification does not longer use the refiner (urrah!)	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	It does not work recursively...	commit \| commitdiff \| tree
2009-09-29	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-09-28	Claudio Sacerdoti...	Experiment...	commit \| commitdiff \| tree
2009-09-28	Claudio Sacerdoti...	Experiment...	commit \| commitdiff \| tree
2009-09-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-09-16	Claudio Sacerdoti...	New interesting coercion.	commit \| commitdiff \| tree
2009-09-16	Claudio Sacerdoti...	The left parameters coming from the constructor types...	commit \| commitdiff \| tree
2009-09-14	Claudio Sacerdoti...	Slightly simplied status code.	commit \| commitdiff \| tree
2009-09-14	Claudio Sacerdoti...	Simplest typing for status records.	commit \| commitdiff \| tree
2009-09-14	Claudio Sacerdoti...	New tactics ncut and nlapply.	commit \| commitdiff \| tree
2009-08-24	Claudio Sacerdoti...	Nicer proof "finished" (up to arithmetical facts).	commit \| commitdiff \| tree
2009-08-21	Claudio Sacerdoti...	Towards a simplified proof.	commit \| commitdiff \| tree
2009-08-21	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-08-20	Claudio Sacerdoti...	Injectivity proved! What a mess...	commit \| commitdiff \| tree
2009-08-20	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-08-20	Claudio Sacerdoti...	- Bug fixed in definition of big_op.	commit \| commitdiff \| tree
next

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

RSS Atom