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

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

2008-10-31	Claudio Sacerdoti...	Environment simplified.	commit \| commitdiff \| tree \| snapshot
2008-10-31	Claudio Sacerdoti...	No longer used.	commit \| commitdiff \| tree \| snapshot
2008-10-31	Claudio Sacerdoti...	- New dependency for environments on the nesting depth.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	Propagation of changes in paramodulation.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	Exported a couple of functions.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	Added a in_universe function	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	propagation of changes in other paramodulation files.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	New demod function working for arbitary goals.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Enrico Tassi	models ported	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	Enforcing the disjoint invariant between metasenvs.	commit \| commitdiff \| tree \| snapshot
2008-10-29	Andrea Asperti	Main change: added a parameter to build_equality_proof...	commit \| commitdiff \| tree \| snapshot
2008-10-28	Enrico Tassi	even more polymorphic dualizer	commit \| commitdiff \| tree \| snapshot
2008-10-28	Enrico Tassi	done	commit \| commitdiff \| tree \| snapshot
2008-10-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-28	Enrico Tassi	lebesge works	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	WIP	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	many bugs fixed	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	metasenv passed to get_relevance, Metas that stand...	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	WIP	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	_ in place of unused variables	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	Implicit annotationas are now printed	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	seg_u/l were inverted, more work	commit \| commitdiff \| tree \| snapshot
2008-10-27	Enrico Tassi	big lemma done	commit \| commitdiff \| tree \| snapshot
2008-10-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-26	Enrico Tassi	duality done	commit \| commitdiff \| tree \| snapshot
2008-10-26	Enrico Tassi	almost done, just needs to be prforated	commit \| commitdiff \| tree \| snapshot
2008-10-26	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2008-10-26	Enrico Tassi	all done in declarative style	commit \| commitdiff \| tree \| snapshot
2008-10-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-25	Enrico Tassi	duality is a joke	commit \| commitdiff \| tree \| snapshot
2008-10-24	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-24	Enrico Tassi	leave-environment axiom made true	commit \| commitdiff \| tree \| snapshot
2008-10-23	Enrico Tassi	lebesgue completely dualized	commit \| commitdiff \| tree \| snapshot
2008-10-22	Ferruccio Guidi	we aligned the implementation to the plmms08 paper	commit \| commitdiff \| tree \| snapshot
2008-10-21	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-21	Enrico Tassi	better pps	commit \| commitdiff \| tree \| snapshot
2008-10-21	Enrico Tassi	- mk_restricted_irl removed, the non-optimized code...	commit \| commitdiff \| tree \| snapshot
2008-10-21	Enrico Tassi	psubst for metas fixed again	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	nat model ported to the dualized version, but not itsel...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	... is a command in proof mode, use	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	more bug fixed (or introduced)	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	after a PITA, lebergue is dualized!	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-20	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	some work on duality, still not finisched	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	grave notation mistake fixed	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	more tests	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-19	Enrico Tassi	when a file is opened the cursor is moved to the begin...	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	tactic language documented;	commit \| commitdiff \| tree \| snapshot
2008-10-18	Ferruccio Guidi	Acic2Procedural:	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	html documentation generation implemented	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	more doc	commit \| commitdiff \| tree \| snapshot
2008-10-18	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-17	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-17	Enrico Tassi	new command eval added	commit \| commitdiff \| tree \| snapshot
2008-10-17	Enrico Tassi	better makefile	commit \| commitdiff \| tree \| snapshot
2008-10-17	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-10-16	Enrico Tassi	ex for students about induction	commit \| commitdiff \| tree \| snapshot
2008-10-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-15	Enrico Tassi	delifting a Meta with an IRL w.r.t. another IRL complet...	commit \| commitdiff \| tree \| snapshot
2008-10-15	Enrico Tassi	some bug fixed	commit \| commitdiff \| tree \| snapshot
2008-10-15	Enrico Tassi	subst_meta was missing	commit \| commitdiff \| tree \| snapshot
2008-10-15	Claudio Sacerdoti...	minor simplification + deps fixed	commit \| commitdiff \| tree \| snapshot
2008-10-15	Claudio Sacerdoti...	New invariant and data structure to represent environme...	commit \| commitdiff \| tree \| snapshot
2008-10-14	Enrico Tassi	more work	commit \| commitdiff \| tree \| snapshot
2008-10-14	Enrico Tassi	firs step for dualization	commit \| commitdiff \| tree \| snapshot
2008-10-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-14	Enrico Tassi	term refinement almost done, some functions exported...	commit \| commitdiff \| tree \| snapshot
2008-10-13	Enrico Tassi	initial refiner ....	commit \| commitdiff \| tree \| snapshot
2008-10-13	Claudio Sacerdoti...	Bug fixed in LetIn: the cumulativity test was performed...	commit \| commitdiff \| tree \| snapshot
2008-10-13	Enrico Tassi	bug in psubst fixed inside local context in Irl form	commit \| commitdiff \| tree \| snapshot
2008-10-13	Enrico Tassi	better error message	commit \| commitdiff \| tree \| snapshot
2008-10-13	Enrico Tassi	ppmetasenv & subst added	commit \| commitdiff \| tree \| snapshot
2008-10-13	Enrico Tassi	NCicReduction.reduce_machine returns a boolean stating...	commit \| commitdiff \| tree \| snapshot
2008-10-08	Wilmer Ricciotti	Fixed a performance problem with unif_machines and...	commit \| commitdiff \| tree \| snapshot
2008-10-06	Enrico Tassi	slow example	commit \| commitdiff \| tree \| snapshot
2008-10-06	Enrico Tassi	3 nasty bugs fixed:	commit \| commitdiff \| tree \| snapshot
2008-10-06	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	better test	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	not so nice patch to small_delta_step	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	when -debug do not catch the exception	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	- NCicPp.ppterm applies the substitution	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	the iterator was wrongly processing the application	commit \| commitdiff \| tree \| snapshot
2008-10-03	Wilmer Ricciotti	Final implementation of proof irrelevant conversion...	commit \| commitdiff \| tree \| snapshot
2008-10-03	Enrico Tassi	better debuggin output	commit \| commitdiff \| tree \| snapshot
2008-10-02	Enrico Tassi	error...	commit \| commitdiff \| tree \| snapshot
2008-10-02	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom