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

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

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
2014-01-09	Ferruccio Guidi	- ynat: some additions	commit \| commitdiff \| tree \| snapshot
2014-01-06	Ferruccio Guidi	one file was missing :)	commit \| commitdiff \| tree \| snapshot
2014-01-06	Ferruccio Guidi	- lleq now uses ynat	commit \| commitdiff \| tree \| snapshot
2014-01-05	Ferruccio Guidi	- new definition of lazy equivalence for local environm...	commit \| commitdiff \| tree \| snapshot
2014-01-03	Ferruccio Guidi	- extended multiple substitutions now uses bounds in...	commit \| commitdiff \| tree \| snapshot
2014-01-03	Ferruccio Guidi	more arithmetics for natural numbers with infinity ...	commit \| commitdiff \| tree \| snapshot
2013-12-28	Ferruccio Guidi	some improvements and new lemmas for	commit \| commitdiff \| tree \| snapshot
2013-12-26	Ferruccio Guidi	the theory of extended multiple substitution for therms...	commit \| commitdiff \| tree \| snapshot
2013-12-20	Ferruccio Guidi	theory of extended iterated substitution begins ...	commit \| commitdiff \| tree \| snapshot
2013-12-19	Ferruccio Guidi	theory of cpy is complete!	commit \| commitdiff \| tree \| snapshot
2013-12-19	Ferruccio Guidi	the theory of cpy continues ...	commit \| commitdiff \| tree \| snapshot
2013-12-17	Ferruccio Guidi	refinement for extended substitution completed	commit \| commitdiff \| tree \| snapshot
2013-12-16	Ferruccio Guidi	- lsubr moved down one component	commit \| commitdiff \| tree \| snapshot
2013-12-15	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-12-15	Ferruccio Guidi	eliminators of arited terms based on "big tree" proper...	commit \| commitdiff \| tree \| snapshot
2013-12-14	Ferruccio Guidi	update in basic_2 completed	commit \| commitdiff \| tree \| snapshot
2013-12-14	Ferruccio Guidi	one file was still missing	commit \| commitdiff \| tree \| snapshot
2013-12-14	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-12-14	Ferruccio Guidi	commit is now complete :)	commit \| commitdiff \| tree \| snapshot
2013-12-14	Ferruccio Guidi	- "big tree" theorem is now proved up to some conjectur...	commit \| commitdiff \| tree \| snapshot
2013-12-09	Ferruccio Guidi	- first results on strongly normalizing local environments	commit \| commitdiff \| tree \| snapshot
2013-12-06	Ferruccio Guidi	partial commit ...	commit \| commitdiff \| tree \| snapshot
2013-12-04	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-12-04	Ferruccio Guidi	third commutation property on lazy equivalence for	commit \| commitdiff \| tree \| snapshot
2013-12-04	Andrea Asperti	New approach: we use "iterator" steps in place of pointers.	commit \| commitdiff \| tree \| snapshot
2013-12-04	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-12-04	Ferruccio Guidi	first and second commutation property on lazy equivalen...	commit \| commitdiff \| tree \| snapshot
2013-12-02	Claudio Sacerdoti...	1. more bugs fixed	commit \| commitdiff \| tree \| snapshot
2013-12-02	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-12-02	Ferruccio Guidi	- last patrtial commit of the "reduction" and "computat...	commit \| commitdiff \| tree \| snapshot
2013-12-02	Claudio Sacerdoti...	More progress.	commit \| commitdiff \| tree \| snapshot
2013-12-02	Claudio Sacerdoti...	Some progress in the correctness proof and a bug fixed.	commit \| commitdiff \| tree \| snapshot
2013-12-02	Ferruccio Guidi	initial commit of the "rduction" component	commit \| commitdiff \| tree \| snapshot
2013-12-01	Ferruccio Guidi	update in ground_2	commit \| commitdiff \| tree \| snapshot
2013-12-01	Ferruccio Guidi	commit of the "substitution" component and of some...	commit \| commitdiff \| tree \| snapshot
2013-12-01	Ferruccio Guidi	- improved arithmetics for natural numbers with infinity	commit \| commitdiff \| tree \| snapshot
2013-11-29	Andrea Asperti	A first example that uses a status monad where the...	commit \| commitdiff \| tree \| snapshot
2013-11-29	Ferruccio Guidi	addition for natural numbers with infinity	commit \| commitdiff \| tree \| snapshot
2013-11-28	Ferruccio Guidi	update in ground_2, web page for ground_2	commit \| commitdiff \| tree \| snapshot
2013-11-28	Ferruccio Guidi	definition of equivalence for local environments,	commit \| commitdiff \| tree \| snapshot
2013-11-27	Ferruccio Guidi	web page for ground_2 and bugfixed statistics generatio...	commit \| commitdiff \| tree \| snapshot
2013-11-27	Ferruccio Guidi	strict order relation for natural numbers with inifinity	commit \| commitdiff \| tree \| snapshot
2013-11-26	Ferruccio Guidi	- natural numbers with infinity for lambdadelta	commit \| commitdiff \| tree \| snapshot
2013-11-25	Ferruccio Guidi	update in ground_2 ...	commit \| commitdiff \| tree \| snapshot
2013-11-25	Ferruccio Guidi	- xoa: the definitions file now includes the notations...	commit \| commitdiff \| tree \| snapshot
2013-11-15	Wilmer Ricciotti	Final version of the binary machine (all proofs completed).	commit \| commitdiff \| tree \| snapshot
2013-11-07	Wilmer Ricciotti	Closes many daemons.	commit \| commitdiff \| tree \| snapshot
2013-11-06	Wilmer Ricciotti	Full rework of the semantics of the binary machine...	commit \| commitdiff \| tree \| snapshot
2013-11-03	Wilmer Ricciotti	Almost finished...	commit \| commitdiff \| tree \| snapshot
2013-11-03	Wilmer Ricciotti	Major bugfix/reorganization/improvement of the partial...	commit \| commitdiff \| tree \| snapshot
2013-11-03	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-11-03	Ferruccio Guidi	second and third commutation property on lazy equivalen...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom