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

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

2009-07-17	Claudio Sacerdoti...	New suffixes for elimination principles:	commit \| commitdiff \| tree
2009-07-17	Claudio Sacerdoti...	1) added a function to retrieve all the universes currently...	commit \| commitdiff \| tree
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	commit \| commitdiff \| tree
2009-07-13	Claudio Sacerdoti...	First proof finished (some tactics still not working).	commit \| commitdiff \| tree
2009-07-13	Claudio Sacerdoti...	Coercion hiding implemented. Notes:	commit \| commitdiff \| tree
2009-07-10	Claudio Sacerdoti...	Composite coercions are here!	commit \| commitdiff \| tree
2009-07-10	Claudio Sacerdoti...	Coercions used here and there.	commit \| commitdiff \| tree
2009-07-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	commit \| commitdiff \| tree
2009-07-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-10	Claudio Sacerdoti...	Let's live with new ocaml type system limitations...	commit \| commitdiff \| tree
2009-07-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-09	Claudio Sacerdoti...	Bug fixed (non-captured variable).	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	eq moved to CProp	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	repeat_tac	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	Hmmmm. This way we need "canonical structures" also...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	Metavariable case in does_not_occur (hence weakly/stricly...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	Missing case for Match implemented.	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	weakly/strictly positive checks relaxed to allow metavariabl...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	Improved error message.	commit \| commitdiff \| tree
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	commit \| commitdiff \| tree
2009-07-07	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2009-07-07	Claudio Sacerdoti...	Bug fixed: one uri was not refreshed, causing divergence...	commit \| commitdiff \| tree
2009-07-07	Claudio Sacerdoti...	Let's play a bit with NG.	commit \| commitdiff \| tree
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively processes...	commit \| commitdiff \| tree
2009-06-23	Claudio Sacerdoti...	Debugging prerr_endlines removed.	commit \| commitdiff \| tree
2009-06-23	Claudio Sacerdoti...	1) NCicTypechecker.typecheck_obj removed, since it...	commit \| commitdiff \| tree
2009-06-23	Claudio Sacerdoti...	- Bug fixed: removed URIs were not removed from the...	commit \| commitdiff \| tree
2009-06-20	Claudio Sacerdoti...	Debugging	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	"matitaclean all" ported to NG	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Invert dependencies between baseuris (files) are now...	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Bug fixed: refreshing of uris for the db.	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	The global db is now updated during decompilation.	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Persistent db (to lookup names in the library) inefficiently...	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	NG decompilation is now activated. However, it is called...	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Estatus finally merged into the global status using...	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Useless GrafiteTypes.get_baseuri removed.	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	More statuses converted to objects.	commit \| commitdiff \| tree
2009-06-19	Claudio Sacerdoti...	Good:	commit \| commitdiff \| tree
2009-06-18	Claudio Sacerdoti...	Objects are now used to represent also the tactic status.	commit \| commitdiff \| tree
2009-06-18	Claudio Sacerdoti...	Stricter type: the type now shows that disambiguation...	commit \| commitdiff \| tree
2009-06-18	Claudio Sacerdoti...	1) grafiteWalker removed	commit \| commitdiff \| tree
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
next

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

RSS Atom