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

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

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
2009-04-06	Enrico Tassi	better error message	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	added one exception	commit \| commitdiff \| tree \| snapshot
2009-04-06	Ferruccio Guidi	- external quantification removed (will be reintroduced...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Ferruccio Guidi	limits: reorganized and attached to nightly tests ...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2009-04-05	Ferruccio Guidi	- Procedural: now we generate the exact tactic (in...	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	New file nTacStatus to:	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	added analyse_indty	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	New tactic "case1_tac" that make "intro" followed by...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	## prefix is now used for tinycals	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	New tactic intro. Syntax: "# n".	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	added tentative elim	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	1) mk_meta now returns also the index of the created...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	removed spurious "	commit \| commitdiff \| tree \| snapshot
2009-03-30	Enrico Tassi	tentative subst-sexpand and change	commit \| commitdiff \| tree \| snapshot
2009-03-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-27	Enrico Tassi	more comments	commit \| commitdiff \| tree \| snapshot
2009-03-27	Enrico Tassi	exec and distribute implemented	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	new apply almost there	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-25	Enrico Tassi	new tactics are almost ready	commit \| commitdiff \| tree \| snapshot
2009-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	add Homepage field	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	set package section to "ocaml"	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	add missing ${misc:Depends}, thanks lintian!	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom