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

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

2014-06-14	Ferruccio Guidi	reorganization of the "static" component:	commit \| commitdiff \| tree \| snapshot
2014-06-10	Ferruccio Guidi	preservation of stratified vaildity through ordinary...	commit \| commitdiff \| tree \| snapshot
2014-06-10	Ferruccio Guidi	update in basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-06-09	Ferruccio Guidi	advances on append allow to complete the long awaited...	commit \| commitdiff \| tree \| snapshot
2014-06-09	Ferruccio Guidi	mailstone in basic_2 !! "big tree" theorem completed...	commit \| commitdiff \| tree \| snapshot
2014-06-08	Ferruccio Guidi	now we use the version of lazy union for local environm...	commit \| commitdiff \| tree \| snapshot
2014-06-08	Ferruccio Guidi	bug fix in lazy union for local environments	commit \| commitdiff \| tree \| snapshot
2014-06-08	Ferruccio Guidi	- some work on append	commit \| commitdiff \| tree \| snapshot
2014-06-07	Ferruccio Guidi	update in basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-06-07	Ferruccio Guidi	source table bugfixed	commit \| commitdiff \| tree \| snapshot
2014-06-07	Ferruccio Guidi	- advances on free variables allow to reduce lleq_lpx_t...	commit \| commitdiff \| tree \| snapshot
2014-06-01	Ferruccio Guidi	- some refactoring and minor additions	commit \| commitdiff \| tree \| snapshot
2014-06-01	Ferruccio Guidi	- advances on hereditarily free variables: now "frees...	commit \| commitdiff \| tree \| snapshot
2014-05-26	Ferruccio Guidi	one file was missing :(	commit \| commitdiff \| tree \| snapshot
2014-05-26	Ferruccio Guidi	new definition of llor gives a long awaited lemma :),	commit \| commitdiff \| tree \| snapshot
2014-05-25	Ferruccio Guidi	update in ground_2 and basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-05-25	Ferruccio Guidi	- theory of llor now includes (long awaited) non-recurs...	commit \| commitdiff \| tree \| snapshot
2014-05-24	Ferruccio Guidi	non-recursive alternative of llpx_sn completed !	commit \| commitdiff \| tree \| snapshot
2014-05-23	Ferruccio Guidi	update in grond_2 and basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-05-23	Ferruccio Guidi	advances on cofrees allows to prove one direction of	commit \| commitdiff \| tree \| snapshot
2014-05-11	Ferruccio Guidi	update in ground_2 and basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-05-11	Ferruccio Guidi	advances on ldrop ....	commit \| commitdiff \| tree \| snapshot
2014-05-10	Ferruccio Guidi	advances on cofrees	commit \| commitdiff \| tree \| snapshot
2014-04-27	Ferruccio Guidi	reordering abstract computation properties and saturati...	commit \| commitdiff \| tree \| snapshot
2014-04-25	Ferruccio Guidi	one file was missing ...	commit \| commitdiff \| tree \| snapshot
2014-04-25	Ferruccio Guidi	- advances in the theory of cofrees	commit \| commitdiff \| tree \| snapshot
2014-04-21	Ferruccio Guidi	- we introduce recursive free variables of a term in...	commit \| commitdiff \| tree \| snapshot
2014-04-20	Ferruccio Guidi	update in basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-04-20	Ferruccio Guidi	- name changes in the rediction rules	commit \| commitdiff \| tree \| snapshot
2014-04-18	Ferruccio Guidi	update in basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-04-18	Ferruccio Guidi	- the relation for pointwise extensions now takes a...	commit \| commitdiff \| tree \| snapshot
2014-04-16	Ferruccio Guidi	anniversary milestone in basic_2 !!	commit \| commitdiff \| tree \| snapshot
2014-04-16	Ferruccio Guidi	3rd anniversary milestone	commit \| commitdiff \| tree \| snapshot
2014-04-15	Ferruccio Guidi	- lazy extended reduction parked	commit \| commitdiff \| tree \| snapshot
2014-04-13	Ferruccio Guidi	we restored the strong normalization of extended comput...	commit \| commitdiff \| tree \| snapshot
2014-04-10	Ferruccio Guidi	commit completed: one file was missing :(	commit \| commitdiff \| tree \| snapshot
2014-04-10	Ferruccio Guidi	- some work on extensions:	commit \| commitdiff \| tree \| snapshot
2014-04-08	Ferruccio Guidi	some advances on pointwise union for local environments ...	commit \| commitdiff \| tree \| snapshot
2014-04-07	Ferruccio Guidi	some resuls on pointwise extensions (all of them are...	commit \| commitdiff \| tree \| snapshot
2014-04-05	Ferruccio Guidi	commit completed:	commit \| commitdiff \| tree \| snapshot
2014-04-02	Ferruccio Guidi	commit of the "computation" component with lazy pointwi...	commit \| commitdiff \| tree \| snapshot
2014-03-30	Ferruccio Guidi	update of the partial commit:	commit \| commitdiff \| tree \| snapshot
2014-03-25	Ferruccio Guidi	- partial commit: just the components below "computation"	commit \| commitdiff \| tree \| snapshot
2014-03-20	Ferruccio Guidi	continuing on lazy pointwise extensions ...	commit \| commitdiff \| tree \| snapshot
2014-03-19	Ferruccio Guidi	we begin to develop lazy pointwisee extensions ...	commit \| commitdiff \| tree \| snapshot
2014-03-11	Ferruccio Guidi	update in ground_2 and basic_2 ...	commit \| commitdiff \| tree \| snapshot
2014-03-11	Ferruccio Guidi	reaxiomatized lleq fixes a bug in it and allows to...	commit \| commitdiff \| tree \| snapshot
2014-03-10	Ferruccio Guidi	some additions ...	commit \| commitdiff \| tree \| snapshot
2014-03-08	Ferruccio Guidi	we define the lazy poinwise extension of a relation...	commit \| commitdiff \| tree \| snapshot
2014-03-08	Ferruccio Guidi	some corrections ...	commit \| commitdiff \| tree \| snapshot
2014-03-07	Claudio Sacerdoti...	Code changed a bit to make it work as before with OCaml...	commit \| commitdiff \| tree \| snapshot
2014-03-07	Claudio Sacerdoti...	Do not assert false for a print not implemented yet.	commit \| commitdiff \| tree \| snapshot
2014-03-07	Claudio Sacerdoti...	Hocus-pocus code to use the old (and deprecated) implem...	commit \| commitdiff \| tree \| snapshot
2014-03-07	Andrea Asperti	Minor changes to make the script more robust to strateg...	commit \| commitdiff \| tree \| snapshot
2014-03-04	Ferruccio Guidi	some external links updated	commit \| commitdiff \| tree \| snapshot
2014-03-04	Ferruccio Guidi	a suggestion was added to avoid 1 pseudo reduction...	commit \| commitdiff \| tree \| snapshot
2014-03-04	Claudio Sacerdoti...	Inclusions improved to allow compilation from the toplevel.	commit \| commitdiff \| tree \| snapshot
2014-03-04	Claudio Sacerdoti...	Bug fixed: the tactic to analyze the term and understan...	commit \| commitdiff \| tree \| snapshot
2014-03-04	Claudio Sacerdoti...	OCaml 4.0 detects a not handled case.	commit \| commitdiff \| tree \| snapshot
2014-03-04	Claudio Sacerdoti...	Different behaviour of OCaml 4.0.	commit \| commitdiff \| tree \| snapshot
2014-03-03	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2014-03-03	Ferruccio Guidi	some additions for the forthcoming presentation	commit \| commitdiff \| tree \| snapshot
2014-02-28	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2014-02-28	Ferruccio Guidi	- some corrections and additions	commit \| commitdiff \| tree \| snapshot
2014-02-27	Claudio Sacerdoti...	Porting of HOTT from Coq to Matita.	commit \| commitdiff \| tree \| snapshot
2014-02-25	Ferruccio Guidi	relabelled documantation entries	commit \| commitdiff \| tree \| snapshot
2014-02-24	Ferruccio Guidi	update in web site and basic_2	commit \| commitdiff \| tree \| snapshot
2014-02-24	Ferruccio Guidi	- we bypassed another false conjecture :) ...	commit \| commitdiff \| tree \| snapshot
2014-02-22	Ferruccio Guidi	addition of unused material :)	commit \| commitdiff \| tree \| snapshot
2014-02-22	Ferruccio Guidi	update in ground_2 and basic_2	commit \| commitdiff \| tree \| snapshot
2014-02-22	Ferruccio Guidi	a wrong conjecture bypassed!	commit \| commitdiff \| tree \| snapshot
2014-02-21	Ferruccio Guidi	update in basic_2 and ground_2	commit \| commitdiff \| tree \| snapshot
2014-02-21	Ferruccio Guidi	- main proposition on lsx finally proved!	commit \| commitdiff \| tree \| snapshot
2014-02-18	Ferruccio Guidi	- a reinforement in a lemma on ldrop allows to prove...	commit \| commitdiff \| tree \| snapshot
2014-02-16	Ferruccio Guidi	- improved definition of lsx allows more invariants	commit \| commitdiff \| tree \| snapshot
2014-02-11	Ferruccio Guidi	update in basic_2 and ground_2	commit \| commitdiff \| tree \| snapshot
2014-02-11	Ferruccio Guidi	some advances on reduction	commit \| commitdiff \| tree \| snapshot
2014-02-04	Ferruccio Guidi	evaluation for context-sensitive extended substitution...	commit \| commitdiff \| tree \| snapshot
2014-02-03	Ferruccio Guidi	we start total substitution ...	commit \| commitdiff \| tree \| snapshot
2014-01-31	Ferruccio Guidi	some notation renamed and fixed	commit \| commitdiff \| tree \| snapshot
2014-01-30	Ferruccio Guidi	normal forms for extended substitution	commit \| commitdiff \| tree \| snapshot
2014-01-29	Ferruccio Guidi	bug fix in the notation of normal forms, now we specify...	commit \| commitdiff \| tree \| snapshot
2014-01-28	Andrea Asperti	Almost there	commit \| commitdiff \| tree \| snapshot
2014-01-28	Andrea Asperti	progress	commit \| commitdiff \| tree \| snapshot
2014-01-27	Ferruccio Guidi	some corrections ...	commit \| commitdiff \| tree \| snapshot
2014-01-27	Andrea Asperti	working version	commit \| commitdiff \| tree \| snapshot
2014-01-26	Ferruccio Guidi	nat: we added a non-indexed theorem	commit \| commitdiff \| tree \| snapshot
2014-01-26	Andrea Asperti	more auxiliary machines	commit \| commitdiff \| tree \| snapshot
2014-01-26	Ferruccio Guidi	- nat: some additions, plus_minus_commutative renamed...	commit \| commitdiff \| tree \| snapshot
2014-01-20	Ferruccio Guidi	milestone in basic_2	commit \| commitdiff \| tree \| snapshot
2014-01-20	Ferruccio Guidi	commit completed: now we support two versions of slicin...	commit \| commitdiff \| tree \| snapshot
2014-01-18	Ferruccio Guidi	- commit of the "reduction" component with two addition...	commit \| commitdiff \| tree \| snapshot
2014-01-17	Ferruccio Guidi	commit of the "unfold" component ...	commit \| commitdiff \| tree \| snapshot
2014-01-17	Ferruccio Guidi	commit of the "static" component	commit \| commitdiff \| tree \| snapshot
2014-01-17	Ferruccio Guidi	- commit of the "substitution" component	commit \| commitdiff \| tree \| snapshot
2014-01-16	Ferruccio Guidi	commit of the "relocation" component with the new defin...	commit \| commitdiff \| tree \| snapshot
2014-01-15	Ferruccio Guidi	we start a criterion on extended computation	commit \| commitdiff \| tree \| snapshot
2014-01-13	Ferruccio Guidi	some improvements on the relation lsx ...	commit \| commitdiff \| tree \| snapshot
2014-01-10	Ferruccio Guidi	update in ground_2 and basic_2	commit \| commitdiff \| tree \| snapshot
2014-01-10	Ferruccio Guidi	new definition of lleq allows to complete the proof...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom