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

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components

[helm.git] / helm / software / components /

2008-11-12	Enrico Tassi	more printings	tree \| commitdiff
2008-11-07	Andrea Asperti	debug=false	tree \| commitdiff
2008-11-07	Andrea Asperti	Signature_of has been closed with respect to constructors.	tree \| commitdiff
2008-11-07	Andrea Asperti	The signature in "retrieve equations" must be extended...	tree \| commitdiff
2008-11-06	Enrico Tassi	do not erase sorts	tree \| commitdiff
2008-11-06	Enrico Tassi	better error messages. sorts are compared using whd	tree \| commitdiff
2008-11-06	Enrico Tassi	Evil case fixed, the coulde should be more readable	tree \| commitdiff
2008-11-06	Enrico Tassi	removed empty lines	tree \| commitdiff
2008-11-06	Enrico Tassi	the passive set and passive list are expected to have...	tree \| commitdiff
2008-11-05	Enrico Tassi	new internal flags for auto:	tree \| commitdiff
2008-11-05	Enrico Tassi	duplicate entry in menv avoided	tree \| commitdiff
2008-11-04	Andrea Asperti	Calling unification instead of matching when checking...	tree \| commitdiff
2008-11-03	Enrico Tassi	removed prerr_endline	tree \| commitdiff
2008-11-03	Enrico Tassi	debug=false	tree \| commitdiff
2008-11-01	Enrico Tassi	added lazy	tree \| commitdiff
2008-10-29	Andrea Asperti	Propagation of changes in paramodulation.	tree \| commitdiff
2008-10-29	Andrea Asperti	Exported a couple of functions.	tree \| commitdiff
2008-10-29	Andrea Asperti	Added a in_universe function	tree \| commitdiff
2008-10-29	Andrea Asperti	propagation of changes in other paramodulation files.	tree \| commitdiff
2008-10-29	Andrea Asperti	New demod function working for arbitary goals.	tree \| commitdiff
2008-10-29	Andrea Asperti	Enforcing the disjoint invariant between metasenvs.	tree \| commitdiff
2008-10-29	Andrea Asperti	Main change: added a parameter to build_equality_proof...	tree \| commitdiff
2008-10-27	Enrico Tassi	many bugs fixed	tree \| commitdiff
2008-10-27	Enrico Tassi	metasenv passed to get_relevance, Metas that stand...	tree \| commitdiff
2008-10-27	Enrico Tassi	_ in place of unused variables	tree \| commitdiff
2008-10-27	Enrico Tassi	Implicit annotationas are now printed	tree \| commitdiff
2008-10-22	Ferruccio Guidi	we aligned the implementation to the plmms08 paper	tree \| commitdiff
2008-10-21	Enrico Tassi	better pps	tree \| commitdiff
2008-10-21	Enrico Tassi	- mk_restricted_irl removed, the non-optimized code...	tree \| commitdiff
2008-10-21	Enrico Tassi	psubst for metas fixed again	tree \| commitdiff
2008-10-20	Enrico Tassi	more bug fixed (or introduced)	tree \| commitdiff
2008-10-20	Enrico Tassi	...	tree \| commitdiff
2008-10-18	Ferruccio Guidi	Acic2Procedural:	tree \| commitdiff
2008-10-17	Enrico Tassi	new command eval added	tree \| commitdiff
2008-10-15	Enrico Tassi	...	tree \| commitdiff
2008-10-15	Enrico Tassi	delifting a Meta with an IRL w.r.t. another IRL complet...	tree \| commitdiff
2008-10-15	Enrico Tassi	some bug fixed	tree \| commitdiff
2008-10-15	Enrico Tassi	subst_meta was missing	tree \| commitdiff
2008-10-14	Enrico Tassi	more work	tree \| commitdiff
2008-10-14	Enrico Tassi	term refinement almost done, some functions exported...	tree \| commitdiff
2008-10-13	Enrico Tassi	initial refiner ....	tree \| commitdiff
2008-10-13	Claudio Sacerdoti...	Bug fixed in LetIn: the cumulativity test was performed...	tree \| commitdiff
2008-10-13	Enrico Tassi	bug in psubst fixed inside local context in Irl form	tree \| commitdiff
2008-10-13	Enrico Tassi	better error message	tree \| commitdiff
2008-10-13	Enrico Tassi	ppmetasenv & subst added	tree \| commitdiff
2008-10-13	Enrico Tassi	NCicReduction.reduce_machine returns a boolean stating...	tree \| commitdiff
2008-10-08	Wilmer Ricciotti	Fixed a performance problem with unif_machines and...	tree \| commitdiff
2008-10-06	Enrico Tassi	slow example	tree \| commitdiff
2008-10-06	Enrico Tassi	3 nasty bugs fixed:	tree \| commitdiff
2008-10-06	Enrico Tassi	...	tree \| commitdiff
2008-10-03	Enrico Tassi	...	tree \| commitdiff
2008-10-03	Enrico Tassi	better test	tree \| commitdiff
2008-10-03	Enrico Tassi	not so nice patch to small_delta_step	tree \| commitdiff
2008-10-03	Enrico Tassi	- NCicPp.ppterm applies the substitution	tree \| commitdiff
2008-10-03	Enrico Tassi	the iterator was wrongly processing the application	tree \| commitdiff
2008-10-03	Wilmer Ricciotti	Final implementation of proof irrelevant conversion...	tree \| commitdiff
2008-10-03	Enrico Tassi	better debuggin output	tree \| commitdiff
2008-10-02	Enrico Tassi	error...	tree \| commitdiff
2008-10-02	Enrico Tassi	...	tree \| commitdiff
2008-10-02	Enrico Tassi	another divergence case patched	tree \| commitdiff
2008-10-02	Enrico Tassi	to avoid a case of divergence small_delta_step checks...	tree \| commitdiff
2008-10-02	Enrico Tassi	...	tree \| commitdiff
2008-10-02	Enrico Tassi	we can test the unification algorithm!	tree \| commitdiff
2008-10-01	Enrico Tassi	commented out unfinished code	tree \| commitdiff
2008-09-30	Enrico Tassi	...	tree \| commitdiff
2008-09-30	Enrico Tassi	unification completed	tree \| commitdiff
2008-09-30	Enrico Tassi	...	tree \| commitdiff
2008-09-30	Ferruccio Guidi	librarian.ml: now the read_only .moo's are managed...	tree \| commitdiff
2008-09-29	Enrico Tassi	quick fix to make read-only baseuri non compiled but...	tree \| commitdiff
2008-09-29	Enrico Tassi	...	tree \| commitdiff
2008-09-26	Enrico Tassi	more push/pop to avoid confusion with imperative data...	tree \| commitdiff
2008-09-26	Ferruccio Guidi	Procedural: we removed some commented code	tree \| commitdiff
2008-09-26	Enrico Tassi	include statement better implemented:	tree \| commitdiff
2008-09-26	Enrico Tassi	auto was compiraing lazy proof terms with = ... fixed	tree \| commitdiff
2008-09-26	Enrico Tassi	iremoved call to auto	tree \| commitdiff
2008-09-26	Enrico Tassi	lazy proof term to increase sharing and decrease memory...	tree \| commitdiff
2008-09-25	Enrico Tassi	...	tree \| commitdiff
2008-09-25	Enrico Tassi	...	tree \| commitdiff
2008-09-25	Enrico Tassi	...	tree \| commitdiff
2008-09-25	Enrico Tassi	beta expand	tree \| commitdiff
2008-09-25	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	added skip function	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-24	Enrico Tassi	...	tree \| commitdiff
2008-09-22	Enrico Tassi	new iterator	tree \| commitdiff
2008-09-21	Ferruccio Guidi	we commented some of the debug pps rather than removing...	tree \| commitdiff
2008-09-19	Enrico Tassi	snapshot	tree \| commitdiff
2008-09-19	Enrico Tassi	snapshot, cicMsubst compiles	tree \| commitdiff
2008-09-19	Enrico Tassi	more abstract discrimination tree	tree \| commitdiff
2008-09-19	Enrico Tassi	added list_seq	tree \| commitdiff
2008-09-19	Enrico Tassi	snapshot	tree \| commitdiff
2008-09-19	Enrico Tassi	better abstraction to allow 1 discrimination tree imple...	tree \| commitdiff
2008-09-19	Enrico Tassi	new discrimination tree	tree \| commitdiff
2008-09-19	Enrico Tassi	Revised discrimination tree implementation:	tree \| commitdiff
2008-09-19	Enrico Tassi	more comments and compare function for URI exported	tree \| commitdiff
next

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

RSS Atom