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

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

2009-06-24	denes	Now inserting hypothesis and goal with zero weight	commit \| commitdiff \| tree \| snapshot
2009-06-24	denes	Extended is_identity test	commit \| commitdiff \| tree \| snapshot
2009-06-24	denes	Implemented check for duplicates (in goals)	commit \| commitdiff \| tree \| snapshot
2009-06-23	denes	Removed old debugging assertion	commit \| commitdiff \| tree \| snapshot
2009-06-23	Ferruccio Guidi	- procedural: basic support for lapply (solves a proble...	commit \| commitdiff \| tree \| snapshot
2009-06-23	denes	Removed debug printing raising Failure	commit \| commitdiff \| tree \| snapshot
2009-06-23	denes	Removed debug printing	commit \| commitdiff \| tree \| snapshot
2009-06-23	denes	Rewrote the main loop for paramodulation	commit \| commitdiff \| tree \| snapshot
2009-06-23	Enrico Tassi	undo/serialization for universes implemented	commit \| commitdiff \| tree \| snapshot
2009-06-23	Claudio Sacerdoti...	Debugging prerr_endlines removed.	commit \| commitdiff \| tree \| snapshot
2009-06-23	Claudio Sacerdoti...	1) NCicTypechecker.typecheck_obj removed, since it...	commit \| commitdiff \| tree \| snapshot
2009-06-23	denes	Fixed nasty bug in maxvar updating	commit \| commitdiff \| tree \| snapshot
2009-06-23	Claudio Sacerdoti...	- Bug fixed: removed URIs were not removed from the...	commit \| commitdiff \| tree \| snapshot
2009-06-23	Enrico Tassi	removed problem not in UEQ	commit \| commitdiff \| tree \| snapshot
2009-06-22	Ferruccio Guidi	- nodes count is now working for aut and meta	commit \| commitdiff \| tree \| snapshot
2009-06-22	denes	Added more precise time information	commit \| commitdiff \| tree \| snapshot
2009-06-22	denes	Added problems from CASC 208	commit \| commitdiff \| tree \| snapshot
2009-06-22	denes	Regenerated problems with corrected tptp2grafite	commit \| commitdiff \| tree \| snapshot
2009-06-22	denes	Corrected proof visiting (topological sort)	commit \| commitdiff \| tree \| snapshot
2009-06-22	denes	Small debugging in tptp2grafite	commit \| commitdiff \| tree \| snapshot
2009-06-21	Wilmer Ricciotti	Added injective compose	commit \| commitdiff \| tree \| snapshot
2009-06-21	Ferruccio Guidi	- cicNotationPp: bugfix in record syntax	commit \| commitdiff \| tree \| snapshot
2009-06-20	Wilmer Ricciotti	Some notation and additional lemmata.	commit \| commitdiff \| tree \| snapshot
2009-06-20	Claudio Sacerdoti...	Debugging	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	"matitaclean all" ported to NG	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Invert dependencies between baseuris (files) are now...	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Bug fixed: refreshing of uris for the db.	commit \| commitdiff \| tree \| snapshot
2009-06-19	Wilmer Ricciotti	More improvements.	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	The global db is now updated during decompilation.	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Persistent db (to lookup names in the library) ineffici...	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	NG decompilation is now activated. However, it is calle...	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Estatus finally merged into the global status using...	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Useless GrafiteTypes.get_baseuri removed.	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	More statuses converted to objects.	commit \| commitdiff \| tree \| snapshot
2009-06-19	Claudio Sacerdoti...	Good:	commit \| commitdiff \| tree \| snapshot
2009-06-18	Enrico Tassi	debug pps removed	commit \| commitdiff \| tree \| snapshot
2009-06-18	Enrico Tassi	better exception handling	commit \| commitdiff \| tree \| snapshot
2009-06-18	Enrico Tassi	proof patching!	commit \| commitdiff \| tree \| snapshot
2009-06-18	Claudio Sacerdoti...	Objects are now used to represent also the tactic status.	commit \| commitdiff \| tree \| snapshot
2009-06-18	denes	Added ntry and nassumption tactics	commit \| commitdiff \| tree \| snapshot
2009-06-18	Enrico Tassi	callbacks were taking in input a status bu were not...	commit \| commitdiff \| tree \| snapshot
2009-06-18	denes	Fixed stupid path	commit \| commitdiff \| tree \| snapshot
2009-06-18	denes	Added script useful for running benchmarks	commit \| commitdiff \| tree \| snapshot
2009-06-18	denes	Changed parenthesis to optional around letin ident...	commit \| commitdiff \| tree \| snapshot
2009-06-18	denes	Fixed wrong types in proof terms	commit \| commitdiff \| tree \| snapshot
2009-06-18	Claudio Sacerdoti...	Stricter type: the type now shows that disambiguation...	commit \| commitdiff \| tree \| snapshot
2009-06-18	Claudio Sacerdoti...	1) grafiteWalker removed	commit \| commitdiff \| tree \| snapshot
2009-06-17	Enrico Tassi	proof reconstruction almost OK	commit \| commitdiff \| tree \| snapshot
2009-06-17	Claudio Sacerdoti...	Initial implementation of statuses using objects in...	commit \| commitdiff \| tree \| snapshot
2009-06-17	denes	Added optionnal one pass simplification (instead of...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	first proof reconstruction attempt, still bugged since it	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	1) unification hint now takes NG terms (as it should...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	1) NCicLibrary (which is untrusted) moved after NCicUnt...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	Implementation of existential type improved (more stric...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	avoid fixing non-recursive terms	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	we fix recursive object reference with the correct...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:	commit \| commitdiff \| tree \| snapshot
2009-06-16	Ferruccio Guidi	we corrected some reduction bugs about renaming.	commit \| commitdiff \| tree \| snapshot
2009-06-15	Ferruccio Guidi	we removed some old code and fixed a reduction bug...	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (part B, by CSC :-):	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (by CSC,actuall :-)	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	added TODO list	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	huge commit regarding the grafite_status:	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	part of last commit	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	tacticals are really tactics now, they have an AST...	commit \| commitdiff \| tree \| snapshot
2009-06-13	Ferruccio Guidi	we removed some coercion detours and we added some...	commit \| commitdiff \| tree \| snapshot
2009-06-12	denes	Implemented keep_simplified.	commit \| commitdiff \| tree \| snapshot
2009-06-12	Claudio Sacerdoti...	ocaml sucks...	commit \| commitdiff \| tree \| snapshot
2009-06-12	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-06-12	Enrico Tassi	-ng implemented	commit \| commitdiff \| tree \| snapshot
2009-06-12	Andrea Asperti	Added a new keep_simplified function	commit \| commitdiff \| tree \| snapshot
2009-06-12	Andrea Asperti	Renamed forward_simplify into simplify and backward_sim...	commit \| commitdiff \| tree \| snapshot
2009-06-11	denes	Active goals are now demodulated after selecting a...	commit \| commitdiff \| tree \| snapshot
2009-06-11	Ferruccio Guidi	- applyTransformation: bugfix in the rendering of records	commit \| commitdiff \| tree \| snapshot
2009-06-11	Enrico Tassi	content2pres for the new cic fixed	commit \| commitdiff \| tree \| snapshot
2009-06-11	Ferruccio Guidi	- some depend files fixed	commit \| commitdiff \| tree \| snapshot
2009-06-10	Ferruccio Guidi	- library/list/list.ma: unused code commented	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	1) added simplification of actives w.r.t. selected	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	right inference step completed	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	new function filter_map_acc	commit \| commitdiff \| tree \| snapshot
2009-06-10	denes	Extended the equality case to non ground terms	commit \| commitdiff \| tree \| snapshot
2009-06-09	Ferruccio Guidi	- Procedural: more support for the Debug inline option...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2009-06-09	Claudio Sacerdoti...	Temporary (and partially broken) patch for Ferruccio...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	almost complete superposition right step	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	see the previous commit	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	termAcicContent is logic independent (despite its name...	commit \| commitdiff \| tree \| snapshot
2009-06-09	denes	Optimized weigths comparison, removed normalization	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	snaphost: supright almost done	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	denes	Implemented substitution application and concatenation	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	fixed metas	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	fixed building	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	a skeleton of supright	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	some more functors and a nice higher-order all_position...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom