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

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

2009-05-06	Ferruccio Guidi	- cicUtil: is_sober now detects folded applications	commit \| commitdiff \| tree \| snapshot
2009-05-06	Enrico Tassi	apply and auto.equational_case call saturation.solve_na...	commit \| commitdiff \| tree \| snapshot
2009-05-06	Enrico Tassi	updated comment	commit \| commitdiff \| tree \| snapshot
2009-05-05	Ferruccio Guidi	- Procedural: new flag "level=n" to control the reconst...	commit \| commitdiff \| tree \| snapshot
2009-05-05	Ferruccio Guidi	- hExtlib: new function "list_assoc_all"	commit \| commitdiff \| tree \| snapshot
2009-05-05	Enrico Tassi	- pretty printer made robust in face of list_nth	commit \| commitdiff \| tree \| snapshot
2009-05-05	Enrico Tassi	more tests	commit \| commitdiff \| tree \| snapshot
2009-05-05	Andrea Asperti	Nuova gestione di "by" per auto.	commit \| commitdiff \| tree \| snapshot
2009-05-05	Andrea Asperti	autobatch by	commit \| commitdiff \| tree \| snapshot
2009-05-01	Ferruccio Guidi	- librarian: 3 bugs fixed in the building system:	commit \| commitdiff \| tree \| snapshot
2009-04-30	Enrico Tassi	run check_if_goal_is_solved on all goals (active+passive)	commit \| commitdiff \| tree \| snapshot
2009-04-30	Matthias Puech	Added an option --enable-annot to the configure to...	commit \| commitdiff \| tree \| snapshot
2009-04-30	Andrea Asperti	Minor changes pro-automation	commit \| commitdiff \| tree \| snapshot
2009-04-30	Andrea Asperti	Added a passive table	commit \| commitdiff \| tree \| snapshot
2009-04-30	Andrea Asperti	Calling paramodulation instead of demod_all	commit \| commitdiff \| tree \| snapshot
2009-04-29	Claudio Sacerdoti...	Refinement of inductive type implemented.	commit \| commitdiff \| tree \| snapshot
2009-04-29	Ferruccio Guidi	- procedural: bugfix in "Barendregt convention" test	commit \| commitdiff \| tree \| snapshot
2009-04-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-29	Enrico Tassi	call paramod instead of solve_Rewrite	commit \| commitdiff \| tree \| snapshot
2009-04-29	Enrico Tassi	no typing	commit \| commitdiff \| tree \| snapshot
2009-04-29	Enrico Tassi	many checks guarded with if Utils.debug_metas	commit \| commitdiff \| tree \| snapshot
2009-04-29	Claudio Sacerdoti...	Records are now interpreted in the NG (but I am sure...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Claudio Sacerdoti...	Inductive definitions are now interpreted (but records...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Claudio Sacerdoti...	Last commit by Ferruccio reverted since it breaks the...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Ferruccio Guidi	cicNotationUtil: in fresh_name_generator, "\eta" replac...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Enrico Tassi	depenalization of smart apply inside auto, that is...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Enrico Tassi	fixed bug, demodulation was keeping results not strictl...	commit \| commitdiff \| tree \| snapshot
2009-04-28	Enrico Tassi	huge commit in automation:	commit \| commitdiff \| tree \| snapshot
2009-04-27	Ferruccio Guidi	matitacLib: bugfix in .moo generation	commit \| commitdiff \| tree \| snapshot
2009-04-26	Claudio Sacerdoti...	The backward compatible management of aliases for NG...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	It is now possible for commands processed by grafiteEng...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Lookup_in_library implemented for new objects. Basicall...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	It is now possible to declare new aliases using the...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Ferruccio Guidi	- matitacLib: lexicon status and grafite status where...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	The translation from old aliases to new references...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Apply subst implemented also for Fixpoints.	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Type for list_index improved.	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Slightly improved type for list_index.	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	New utility function list_index (useful in many places...	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Better error message.	commit \| commitdiff \| tree \| snapshot
2009-04-25	Claudio Sacerdoti...	Debug option reverted.	commit \| commitdiff \| tree \| snapshot
2009-04-25	Ferruccio Guidi	- matitacLib: better handling of the callbacks for...	commit \| commitdiff \| tree \| snapshot
2009-04-24	Claudio Sacerdoti...	- Grammar for all obj commands ported to NG (let recs...	commit \| commitdiff \| tree \| snapshot
2009-04-24	Claudio Sacerdoti...	Quick&dirty implementation of neqd:	commit \| commitdiff \| tree \| snapshot
2009-04-22	Ferruccio Guidi	- transcript: we have now two styles of mma's from...	commit \| commitdiff \| tree \| snapshot
2009-04-22	Wilmer Ricciotti	syntax colouring for inverters	commit \| commitdiff \| tree \| snapshot
2009-04-22	Wilmer Ricciotti	Disabled debug prints in the inversion principle.	commit \| commitdiff \| tree \| snapshot
2009-04-22	Wilmer Ricciotti	New command "inverter" used to generate an induction...	commit \| commitdiff \| tree \| snapshot
2009-04-22	Enrico Tassi	demodulate takes an extra argument 'all', if present...	commit \| commitdiff \| tree \| snapshot
2009-04-21	Ferruccio Guidi	- MatitaMisc: we factorized here the function out_pream...	commit \| commitdiff \| tree \| snapshot
2009-04-21	Enrico Tassi	fixed last file restricting auto tables	commit \| commitdiff \| tree \| snapshot
2009-04-20	Enrico Tassi	- init_cache_and_tables rewritten using the automation_...	commit \| commitdiff \| tree \| snapshot
2009-04-20	Claudio Sacerdoti...	Bug fixed: variable capture in previous commit prevente...	commit \| commitdiff \| tree \| snapshot
2009-04-17	Claudio Sacerdoti...	Some improvements.	commit \| commitdiff \| tree \| snapshot
2009-04-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Ferruccio Guidi	Procedural: we corrected two errors about the handling...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	Bug: let-ins are always automatically folded!	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	test/a.ma => tests/ng_tactics.ma, with nassert here...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	Replaced long, bugged implementation of letin-tac with...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	Added ppterm.	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	The context is now parsed in the reverse (right) order.	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Enrico Tassi	Universe is used only locally to tactics/	commit \| commitdiff \| tree \| snapshot
2009-04-16	Enrico Tassi	added an exception	commit \| commitdiff \| tree \| snapshot
2009-04-15	Ferruccio Guidi	- transcript: bugfix	commit \| commitdiff \| tree \| snapshot
2009-04-14	Ferruccio Guidi	we rebuilt the dependences	commit \| commitdiff \| tree \| snapshot
2009-04-14	Ferruccio Guidi	- Procedural: generation of "exact" is now complete	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	Trick: the refiner always subst-expands the outtype...	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	Bug fixed in two lines + 5 lines of comment.	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	assert_tac now takes a list of sequents and also checks...	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	New debugging tactic nassert:	commit \| commitdiff \| tree \| snapshot
2009-04-12	Claudio Sacerdoti...	Semantic selection back again (but no semantic cut...	commit \| commitdiff \| tree \| snapshot
2009-04-12	Claudio Sacerdoti...	Match is now rendered as best as possible.	commit \| commitdiff \| tree \| snapshot
2009-04-10	Claudio Sacerdoti...	The sequent viewer now considers the context to render...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Ferruccio Guidi	- character: we adjusted some "autobatch" parameters	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	The substitution is now taken in account when printing...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	added letin, still broken	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	new tactic whd implemented	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	- change implemented in 4 lines	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	- generalize finished	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	?_OS1 := C[ ?_IN ]	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	fixed modules order	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	minor fixes	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	+ Chain NCic.term -> content -> presentation very...	commit \| commitdiff \| tree \| snapshot
2009-04-08	Claudio Sacerdoti...	Just to make it compile again.	commit \| commitdiff \| tree \| snapshot
2009-04-08	Enrico Tassi	generalized is half-implemented (still broken)	commit \| commitdiff \| tree \| snapshot
2009-04-08	Enrico Tassi	Analizyng the inductive type of the eliminated term and	commit \| commitdiff \| tree \| snapshot
2009-04-07	Claudio Sacerdoti...	- nrewrite ((very?) rough implementation)	commit \| commitdiff \| tree \| snapshot
2009-04-07	Claudio Sacerdoti...	- more progress towards generalize, but I am stuck now	commit \| commitdiff \| tree \| snapshot
2009-04-07	Enrico Tassi	- select_tac honors the hypotheses pattern when require...	commit \| commitdiff \| tree \| snapshot
2009-04-07	Enrico Tassi	select honors the substitution	commit \| commitdiff \| tree \| snapshot
2009-04-06	Claudio Sacerdoti...	New tactic clear; new syntax # _; to introduce and...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	tactic cases works! delift clears tags	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	eta-contraction was made on the wrong term	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	unification:	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom