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

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

2009-05-14	Ferruccio Guidi	- hExtlib: added debugging information for split_nth	commit \| commitdiff \| tree \| snapshot
2009-05-14	Ferruccio Guidi	- libraryObjects: new default "natural numbers" with...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Ferruccio Guidi	interpretations placed right after the corresponding...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Ferruccio Guidi	- matitaEngine: some commands like "coercion" must...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	The singature of the "by" universe is added to the...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Via un'altra linea...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Sempre piu' breve	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Signature is computed on the initial goal, once and...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Claudio Sacerdoti...	Do we really want to generate eliminators for nested...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Claudio Sacerdoti...	All weakly positive types but imbricated ones are now...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Ferruccio Guidi	- Procedural: we now reconstruct "let H := v in t"...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Andrea Asperti	We only filter the smart candidates w.r.t the signature	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Some experiments in generation of elimination principles.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	ppsubst commented out in ppobj	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Bug fixed: the relevance list can be shorted then leftn...	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Missing spaces inserted here and there.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	- non_punctuational_tacticals ported to NG	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Buffers are now used everywhere for speed-up.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	New function list_iter_sep.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Andrea Asperti	A few lemmas about inclusion.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Andrea Asperti	More automation	commit \| commitdiff \| tree \| snapshot
2009-05-10	Claudio Sacerdoti...	- critical bug fixed in NCicSubstitution.lift:	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Stupid typing error fixed.	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed: left parameters of constructors were unified...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed: refinement of mutual recursive definitions...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Improved tests (for left parameters and mutual recursiv...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed in refinement of inductive types: left parame...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	1) better implementation of NObj that now calls recursi...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	The relevance list can be shorter than leftno (when...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed in interpretation of records (the type was...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Andrea Asperti	Constructors are closed with thier types when computing...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Andrea Asperti	versione automatizzata	commit \| commitdiff \| tree \| snapshot
2009-05-08	Andrea Asperti	symmetry of inequality sym_neq	commit \| commitdiff \| tree \| snapshot
2009-05-07	Ferruccio Guidi	documentation for the inline command	commit \| commitdiff \| tree \| snapshot
2009-05-06	Ferruccio Guidi	- dependenciesParser: updated to new inline syntax	commit \| commitdiff \| tree \| snapshot
2009-05-06	Ferruccio Guidi	LAMBDA-TYPES: mma's recommitted because inline syntax...	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom