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

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

2008-04-07	Enrico Tassi	the explicit type in a LetIn must be typecheckd before...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	opt compilation enabled, removed some pps, check has...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	lefts_ad_tys properly sorted, added some metasenv here...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	lefts_and_tys was tys@lefts, CSC claims it was working...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added a list of uris to ease debugging	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	print the excpetion and raise it again, seems to produc...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	new constants have depth = max_int insted of 0 so that...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	off by one in calling count_from	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	fixed bug in translating Fix, recno was not properly...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added a pretty printing of the new object and use argv...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	context, metasenv and subst made mandatory in CicPp	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	guarded by has a nice error message	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	reference type made private, added mk_constructor to...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	some debug printings	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added to the cache a boolean to state if the object is	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	fix	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	today it seems that the substituted should be lifted...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added ppobj	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type_of_constant was retunrning the type of the wrong...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	fixed list.nth and added some paretheses	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added some printings and catched more exceptions	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	removed useless printing	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	iterator map was mapping Lambdas to Prods!!!	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	debugging started	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type of constant ported	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added add_obj to store objects in the environment,...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	logger added	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added get_obj in nCicEnvironment that returns an object...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	indentation fixed	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	returns_a_counductive implemented	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type_of_branch ported and optimized to not lift the...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	is_really_smaller ported, still to understand the case...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	debujin implemented with the map recursor	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	bug found rewriting the kernel backported: n instead...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	non debruijned constructor may be useless elswere,...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	guarded_by_destructor ported, many auxiliary functions...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	removed FSF banner	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	added ugly test showing many many bugs in the current...	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	added slim version of does_not_occur	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	added translation of Set to Type0 (avoid warning)	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixes backported from the new kernel	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrite	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrite	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrites	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixed according to the new rewrite semantics (fails...	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixed depends after the removal of Fsub	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	better check for progress	commit \| commitdiff \| tree \| snapshot
2008-04-01	Claudio Sacerdoti...	typeof_obj0 implemented	commit \| commitdiff \| tree \| snapshot
2008-04-01	Claudio Sacerdoti...	1) added get_checked_indtys that returns the whole...	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	progress made better, still not perfect	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added to rewrite a check to effectively do something...	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added some comments, but the samentics of many function...	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added set_ppterm	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	Automatic generation of elimination and inversion princ...	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	Large amount of duplicated code (still in comments...	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	1) Impredicative sort "Set" removed everywhere.	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	1) more sharing everywhere in NCicSubstitution	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	more cases of the type checker honoured, still missing...	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	added is_closed to nCicUtils.	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	moved psubst and list to the new iterators, result...	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	added iterators over NCic terms	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	removed FSF header	commit \| commitdiff \| tree \| snapshot
2008-03-27	Wilmer Ricciotti	Updated depedencies.	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	insert comments of old tpechecker	commit \| commitdiff \| tree \| snapshot
2008-03-26	Wilmer Ricciotti	Reorganization of list library (step 1)	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	new are_convertible and head_beta_reduce	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	context for fixpoint body created in the hopefully...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	ported to the Cic LetIn with explicit type	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	this patch is a shit, the part that fixes the heuristic...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	fix with m (to be optimized) are rewritten such that...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	very very interesting hack	commit \| commitdiff \| tree \| snapshot
2008-03-25	Wilmer Ricciotti	small update	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	argument of type mcu_type always abstracted first	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	XXX this is the beginning of the metaocaml work XXX	commit \| commitdiff \| tree \| snapshot
2008-03-23	Enrico Tassi	Fsub moved in contribs	commit \| commitdiff \| tree \| snapshot
2008-03-23	Ferruccio Guidi	cicNotationPp: fixed letin syntax (now typeless)	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	since many stuff is under contrib, we need to ignore...	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	library_auto moved inside contrib, still not ported...	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	moved dama/ and dama_didactic/ in contribs/dama/	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	freescale moved under contribs. contribs made relocatable	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	New syntax for auto-related tactics and conclude/obtain.	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	Script fixed (it did not compile due to a mistake befor...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Ferruccio Guidi	Base-2 is not compiling properly and is excluded for now	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	changed auto_tac params type and all derivate tactics...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	new semantics for 'by t'	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	removed pointless test	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	I believe that auto paramodulation does not try to	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	added library option to auto	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	letins are no more unfolded, we do that by hand	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	letin are no longer unfolded thus coercions not propaga...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	End of patch for computation of LetIn types. Now types...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Bug: types and terms pushed into the context must be...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	-debug improved	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Number notation for Coq is back again, waiting for...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Files committed by Enrico (a mistake, I suppose) removed.	commit \| commitdiff \| tree \| snapshot
2008-03-19	Ferruccio Guidi	Procedural : added some missing cases	commit \| commitdiff \| tree \| snapshot
2008-03-18	Ferruccio Guidi	LAMBDA-TYPES: level 2 dependences are now correct,...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom