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

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

2009-05-11	Claudio Sacerdoti...	- non_punctuational_tacticals ported to NG	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	Buffers are now used everywhere for speed-up.	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	New function list_iter_sep.	commit \| commitdiff \| tree
2009-05-10	Claudio Sacerdoti...	- critical bug fixed in NCicSubstitution.lift:	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Stupid typing error fixed.	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Bug fixed: left parameters of constructors were unified...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Bug fixed: refinement of mutual recursive definitions...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Improved tests (for left parameters and mutual recursive...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Bug fixed in refinement of inductive types: left parameters...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	1) better implementation of NObj that now calls recursively...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	The relevance list can be shorter than leftno (when...	commit \| commitdiff \| tree
2009-05-08	Claudio Sacerdoti...	Bug fixed in interpretation of records (the type was...	commit \| commitdiff \| tree
2009-04-29	Claudio Sacerdoti...	Refinement of inductive type implemented.	commit \| commitdiff \| tree
2009-04-29	Claudio Sacerdoti...	Records are now interpreted in the NG (but I am sure...	commit \| commitdiff \| tree
2009-04-28	Claudio Sacerdoti...	Inductive definitions are now interpreted (but records...	commit \| commitdiff \| tree
2009-04-28	Claudio Sacerdoti...	Last commit by Ferruccio reverted since it breaks the...	commit \| commitdiff \| tree
2009-04-26	Claudio Sacerdoti...	The backward compatible management of aliases for NG...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	It is now possible for commands processed by grafiteEngine...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Lookup_in_library implemented for new objects. Basically...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	It is now possible to declare new aliases using the...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	The translation from old aliases to new references...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Apply subst implemented also for Fixpoints.	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Type for list_index improved.	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Slightly improved type for list_index.	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	New utility function list_index (useful in many places...	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Better error message.	commit \| commitdiff \| tree
2009-04-25	Claudio Sacerdoti...	Debug option reverted.	commit \| commitdiff \| tree
2009-04-24	Claudio Sacerdoti...	- Grammar for all obj commands ported to NG (let recs...	commit \| commitdiff \| tree
2009-04-24	Claudio Sacerdoti...	Quick&dirty implementation of neqd:	commit \| commitdiff \| tree
2009-04-20	Claudio Sacerdoti...	Bug fixed: variable capture in previous commit prevented...	commit \| commitdiff \| tree
2009-04-17	Claudio Sacerdoti...	Some improvements.	commit \| commitdiff \| tree
2009-04-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	Bug: let-ins are always automatically folded!	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	test/a.ma => tests/ng_tactics.ma, with nassert here...	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	Replaced long, bugged implementation of letin-tac with...	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	Added ppterm.	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	The context is now parsed in the reverse (right) order.	commit \| commitdiff \| tree
2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-14	Claudio Sacerdoti...	Trick: the refiner always subst-expands the outtype...	commit \| commitdiff \| tree
2009-04-14	Claudio Sacerdoti...	Bug fixed in two lines + 5 lines of comment.	commit \| commitdiff \| tree
2009-04-14	Claudio Sacerdoti...	assert_tac now takes a list of sequents and also checks...	commit \| commitdiff \| tree
2009-04-14	Claudio Sacerdoti...	New debugging tactic nassert:	commit \| commitdiff \| tree
2009-04-12	Claudio Sacerdoti...	Semantic selection back again (but no semantic cut...	commit \| commitdiff \| tree
2009-04-12	Claudio Sacerdoti...	Match is now rendered as best as possible.	commit \| commitdiff \| tree
2009-04-10	Claudio Sacerdoti...	The sequent viewer now considers the context to render...	commit \| commitdiff \| tree
2009-04-09	Claudio Sacerdoti...	The substitution is now taken in account when printing...	commit \| commitdiff \| tree
2009-04-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-09	Claudio Sacerdoti...	+ Chain NCic.term -> content -> presentation very...	commit \| commitdiff \| tree
2009-04-08	Claudio Sacerdoti...	Just to make it compile again.	commit \| commitdiff \| tree
2009-04-07	Claudio Sacerdoti...	- nrewrite ((very?) rough implementation)	commit \| commitdiff \| tree
2009-04-07	Claudio Sacerdoti...	- more progress towards generalize, but I am stuck now	commit \| commitdiff \| tree
2009-04-06	Claudio Sacerdoti...	New tactic clear; new syntax # _; to introduce and...	commit \| commitdiff \| tree
2009-04-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-01	Claudio Sacerdoti...	New tactic "case1_tac" that make "intro" followed by...	commit \| commitdiff \| tree
2009-04-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-04-01	Claudio Sacerdoti...	## prefix is now used for tinycals	commit \| commitdiff \| tree
2009-04-01	Claudio Sacerdoti...	New tactic intro. Syntax: "# n".	commit \| commitdiff \| tree
2009-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-03-12	Claudio Sacerdoti...	More details on the proof.	commit \| commitdiff \| tree
2009-03-12	Claudio Sacerdoti...	New algorithm based on in-place modification of the...	commit \| commitdiff \| tree
2009-03-06	Claudio Sacerdoti...	Minor improvements in pretty-printing.	commit \| commitdiff \| tree
2009-03-05	Claudio Sacerdoti...	New version: only new nodes are normalized; moreover...	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	First version.	commit \| commitdiff \| tree
2009-03-02	Claudio Sacerdoti...	Old algorithm moved to old to leave place to the new...	commit \| commitdiff \| tree
2009-02-02	Claudio Sacerdoti...	Hmmm, going too low.	commit \| commitdiff \| tree
2009-02-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-02-01	Claudio Sacerdoti...	Towards fullness.	commit \| commitdiff \| tree
2009-02-01	Claudio Sacerdoti...	Renaming.	commit \| commitdiff \| tree
2009-02-01	Claudio Sacerdoti...	Renaming.	commit \| commitdiff \| tree
2009-01-22	Claudio Sacerdoti...	TODO	commit \| commitdiff \| tree
2009-01-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-01-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-01-18	Claudio Sacerdoti...	universe inconsistency fixed	commit \| commitdiff \| tree
2009-01-18	Claudio Sacerdoti...	SUBSETS_full up to universe inconsistency	commit \| commitdiff \| tree
2009-01-17	Claudio Sacerdoti...	faithful	commit \| commitdiff \| tree
2009-01-17	Claudio Sacerdoti...	CAT2	commit \| commitdiff \| tree
2009-01-16	Claudio Sacerdoti...	Sambin's result holds trivially since most of the fields...	commit \| commitdiff \| tree
2009-01-16	Claudio Sacerdoti...	basic topologies are trivially o-basic topologies	commit \| commitdiff \| tree
2009-01-16	Claudio Sacerdoti...	1. new coercion(s) from CPropi to CProp	commit \| commitdiff \| tree
2009-01-14	Claudio Sacerdoti...	o_continous_relations are really o_relation_pair.....	commit \| commitdiff \| tree
2009-01-14	Claudio Sacerdoti...	o-basic_pairs are indeed examples of o-basic_topologies!	commit \| commitdiff \| tree
2009-01-13	Claudio Sacerdoti...	- Added new output in standard C.	commit \| commitdiff \| tree
2009-01-12	Claudio Sacerdoti...	Some work on o-algebras towards the proof that a and...	commit \| commitdiff \| tree
2009-01-08	Claudio Sacerdoti...	The new coercion from SET to Type0 with higher priority...	commit \| commitdiff \| tree
2009-01-08	Claudio Sacerdoti...	Just a snapshot.	commit \| commitdiff \| tree
2009-01-06	Claudio Sacerdoti...	More work on concrete spaces.	commit \| commitdiff \| tree
2009-01-06	Claudio Sacerdoti...	Some work on concrete spaces.	commit \| commitdiff \| tree
2009-01-06	Claudio Sacerdoti...	Cool: only 8 universes in use.	commit \| commitdiff \| tree
next

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

RSS Atom