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

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

2007-05-17	Enrico Tassi	added a (for the moment) dummy field _subst to ProofengineTy...	commit \| commitdiff \| tree
2007-05-17	Enrico Tassi	auto rewritten with only one tail recursive function.	commit \| commitdiff \| tree
2007-05-17	Enrico Tassi	OPT tests restored	commit \| commitdiff \| tree
2007-05-07	Enrico Tassi	...	commit \| commitdiff \| tree
2007-05-07	Enrico Tassi	a bit of sharing and the optimization of not folding...	commit \| commitdiff \| tree
2007-05-07	Enrico Tassi	some minor fixes done in cividale (bugfix coming from...	commit \| commitdiff \| tree
2007-04-20	Enrico Tassi	developments root are now part of default inclusion...	commit \| commitdiff \| tree
2007-04-20	Enrico Tassi	added library_auto/ to tests.	commit \| commitdiff \| tree
2007-04-20	Enrico Tassi	fixed paths and prefixes of included files	commit \| commitdiff \| tree
2007-04-18	Enrico Tassi	more discriminate	commit \| commitdiff \| tree
2007-04-18	Enrico Tassi	handles failures (sometimes you can't inject)	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	one more step toward a decent destruct	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	RT_BASEDIR changed to a sensible path	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	broken list fix	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	fixed a list.nth called on a too short list	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	...	commit \| commitdiff \| tree
2007-04-17	Enrico Tassi	added generation of hne and heq problems	commit \| commitdiff \| tree
2007-04-16	Enrico Tassi	better simplify	commit \| commitdiff \| tree
2007-04-16	Enrico Tassi	simplify has a brand new semantics!	commit \| commitdiff \| tree
2007-04-16	Enrico Tassi	closed all axioms	commit \| commitdiff \| tree
2007-04-12	Enrico Tassi	HACK for indtype checking	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	fixed case	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	set -> type	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	...	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	...	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	...	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	match x in IDENT and not TERM	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	still not completely working but at least non dumb...	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	you can case even if only a right appears... so, substitutin...	commit \| commitdiff \| tree
2007-04-10	Enrico Tassi	...	commit \| commitdiff \| tree
2007-04-06	Enrico Tassi	eval_from_stream is now tail recursive!	commit \| commitdiff \| tree
2007-04-05	Enrico Tassi	pattern with match fixed	commit \| commitdiff \| tree
2007-04-05	Enrico Tassi	many printings added	commit \| commitdiff \| tree
2007-04-05	Enrico Tassi	fixed the pretty (notation aware) printer	commit \| commitdiff \| tree
2007-04-03	Enrico Tassi	new case implementation	commit \| commitdiff \| tree
2007-04-02	Enrico Tassi	added some tests for cases	commit \| commitdiff \| tree
2007-04-02	Enrico Tassi	hopefully fixed cases implementation	commit \| commitdiff \| tree
2007-03-26	Enrico Tassi	added eta expansion to avoid universe inconsistency.	commit \| commitdiff \| tree
2007-02-19	Enrico Tassi	added some code to print the praamodulation proofs...	commit \| commitdiff \| tree
2007-02-01	Enrico Tassi	restored coercions between eq and eq	commit \| commitdiff \| tree
2007-02-01	Enrico Tassi	reverted a commented substitution in build_newgoal...	commit \| commitdiff \| tree
2007-01-06	Enrico Tassi	- inside dicrimination_tree is now checked the invariant...	commit \| commitdiff \| tree
2007-01-06	Enrico Tassi	;auto fixed	commit \| commitdiff \| tree
2007-01-05	Enrico Tassi	removed debugging printing	commit \| commitdiff \| tree
2007-01-05	Enrico Tassi	debuggin message improved	commit \| commitdiff \| tree
2007-01-05	Enrico Tassi	add_moo_content does not add a coercion statement twice	commit \| commitdiff \| tree
2007-01-05	Enrico Tassi	Added check for duplicate (convertible) composite coercions,	commit \| commitdiff \| tree
2007-01-05	Enrico Tassi	Erroneously declared coercion removed	commit \| commitdiff \| tree
2007-01-03	Enrico Tassi	oder tests	commit \| commitdiff \| tree
2007-01-02	Enrico Tassi	added oblivion_universe and used it in paxck_coercions	commit \| commitdiff \| tree
2006-12-22	Enrico Tassi	Speeedup! (by caching)	commit \| commitdiff \| tree
2006-12-21	Enrico Tassi	added some missing includes	commit \| commitdiff \| tree
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree
2006-11-25	Enrico Tassi	fix	commit \| commitdiff \| tree
2006-11-25	Enrico Tassi	patch to calculate meets of a pair of carriers	commit \| commitdiff \| tree
2006-11-25	Enrico Tassi	added assertion (that is a TODO) in case non-considered...	commit \| commitdiff \| tree
2006-11-25	Enrico Tassi	added a test for the pullback stuff and the possibility...	commit \| commitdiff \| tree
2006-10-24	Enrico Tassi	fixed the ugly button added by csc, now it is inside...	commit \| commitdiff \| tree
2006-10-24	Enrico Tassi	removed equality_retrieval	commit \| commitdiff \| tree
2006-10-12	Enrico Tassi	carr_of_term now returns Fun if a Prod is encountered	commit \| commitdiff \| tree
2006-10-12	Enrico Tassi	fixed defaultauto behaviour. not the cache is preserveed	commit \| commitdiff \| tree
2006-10-12	Enrico Tassi	timeout if unspecfied should be set to infinity, not...	commit \| commitdiff \| tree
2006-10-06	Enrico Tassi	added support for short name targets	commit \| commitdiff \| tree
2006-10-06	Enrico Tassi	resumed ol auto	commit \| commitdiff \| tree
2006-10-06	Enrico Tassi	fixed all (that now uses long paths)	commit \| commitdiff \| tree
2006-10-06	Enrico Tassi	now the makefile for developments requires the depend...	commit \| commitdiff \| tree
2006-10-03	Enrico Tassi	reduced timeout to 100s	commit \| commitdiff \| tree
2006-10-03	Enrico Tassi	commented out are_convertible in is_identity	commit \| commitdiff \| tree
2006-10-03	Enrico Tassi	Query fixed to handle the cases where 0 tests are failures...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	restored is_identity instead of is_weak_identity	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	added a subtle List.rev that makes the order of the...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	auto always uses the context (even if paramodulation...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	returns the right list of goals	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	50 steps on goal are fine for irrat2	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	removed only made with the DB	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	removed a pointless call to auto	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	added tests for paramod	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	...	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	added missing *)	commit \| commitdiff \| tree
2006-10-02	Enrico Tassi	restored old (r6662) behaviour	commit \| commitdiff \| tree
2006-10-01	Enrico Tassi	when use_only_paramod is true do not calculate the...	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	2: is_identity -> is_weak_identity	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	fixed metaconvertibility that was completely wrong.	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	removed bad guard that was always false (assert false...	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	fixed (dasabled paramod)	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	renamed inference in founif that is more appropriate	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	is_identity -> is_weak_identity	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	hack to make the Pp work (sometimes)	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	new version of auto that is able to prove the irrationality...	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	added tests for auto	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	restored the good factorization file	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	ported to the new reflexivity implementation	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	maittaprover uses another format	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	...	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	removed a useless printing	commit \| commitdiff \| tree
2006-09-29	Enrico Tassi	added metas local context maction: ?n[...]	commit \| commitdiff \| tree
next

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

RSS Atom