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

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

2009-06-17	Claudio Sacerdoti...	Initial implementation of statuses using objects in...	commit \| commitdiff \| tree
2009-06-16	Claudio Sacerdoti...	1) unification hint now takes NG terms (as it should...	commit \| commitdiff \| tree
2009-06-16	Claudio Sacerdoti...	1) NCicLibrary (which is untrusted) moved after NCicUntrusted.	commit \| commitdiff \| tree
2009-06-16	Claudio Sacerdoti...	Implementation of existential type improved (more strict...	commit \| commitdiff \| tree
2009-06-16	Claudio Sacerdoti...	FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:	commit \| commitdiff \| tree
2009-06-12	Claudio Sacerdoti...	ocaml sucks...	commit \| commitdiff \| tree
2009-06-12	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-06-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2009-06-09	Claudio Sacerdoti...	Temporary (and partially broken) patch for Ferruccio...	commit \| commitdiff \| tree
2009-06-06	Claudio Sacerdoti...	Previous commit reverted, as explained in that log.	commit \| commitdiff \| tree
2009-06-06	Claudio Sacerdoti...	This commit restores the ids_to_father_ids table.	commit \| commitdiff \| tree
2009-06-05	Claudio Sacerdoti...	1) the home button of CicBrowser now works also for NG	commit \| commitdiff \| tree
2009-06-05	Claudio Sacerdoti...	The kernel _must_ check the correctness of the height...	commit \| commitdiff \| tree
2009-06-03	Claudio Sacerdoti...	New test for NG notation.	commit \| commitdiff \| tree
2009-06-03	Claudio Sacerdoti...	Huge commit with several changes:	commit \| commitdiff \| tree
2009-05-27	Claudio Sacerdoti...	Basic support for interpretations for NG:	commit \| commitdiff \| tree
2009-05-26	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-05-26	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-05-18	Claudio Sacerdoti...	removed byte queries	commit \| commitdiff \| tree
2009-05-18	Claudio Sacerdoti...	1) GrafiteAst.NEval => GrafiteAst.NReduce	commit \| commitdiff \| tree
2009-05-18	Claudio Sacerdoti...	1) new tactic normalize (low-level function implemented in	commit \| commitdiff \| tree
2009-05-18	Claudio Sacerdoti...	1) order of processing of case branches reverted (to...	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	maxmeta implemented	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	maxmeta function to return the heighest meta used so far	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	alpha_eq exported	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	alpha_eq defined and exported	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	efficiency improvement (buffers are now used everywhere)	commit \| commitdiff \| tree
2009-05-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-05-15	Claudio Sacerdoti...	Patch to add a debugging string to HExtlib.split_nth...	commit \| commitdiff \| tree
2009-05-15	Claudio Sacerdoti...	Cosmetic.	commit \| commitdiff \| tree
2009-05-12	Claudio Sacerdoti...	Do we really want to generate eliminators for nested...	commit \| commitdiff \| tree
2009-05-12	Claudio Sacerdoti...	All weakly positive types but imbricated ones are now...	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	Some experiments in generation of elimination principles.	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	ppsubst commented out in ppobj	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	Bug fixed: the relevance list can be shorted then leftno...	commit \| commitdiff \| tree
2009-05-11	Claudio Sacerdoti...	Missing spaces inserted here and there.	commit \| commitdiff \| tree
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
next

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

RSS Atom