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

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

2013-02-04	Claudio Sacerdoti...	Bug fixed: the indty can be typed with a Prod, not...	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	New option -extract_ocaml to extract to ocaml files.	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Pretty printing of ocaml files slightly improved.	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Last known bug unrelated to names fixed: a fixpoint...	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2013-02-02	Claudio Sacerdoti...	Makefile to extract to ocaml code.	commit \| commitdiff \| tree
2013-02-02	Claudio Sacerdoti...	Oops, part of last commit (ocaml extraction implementation)	commit \| commitdiff \| tree
2013-02-02	Claudio Sacerdoti...	Ooops, this completes the previous commit (ocaml extraction...	commit \| commitdiff \| tree
2013-02-02	Claudio Sacerdoti...	Implementation of Ocaml extraction (largely ported...	commit \| commitdiff \| tree
2013-02-02	Claudio Sacerdoti...	Identity change, improves readability.	commit \| commitdiff \| tree
2012-12-06	Claudio Sacerdoti...	Bug fixed: %n was badly failing (with Failure "nth...	commit \| commitdiff \| tree
2012-10-19	Claudio Sacerdoti...	One useless Obj.magic removed.	commit \| commitdiff \| tree
2012-09-19	Claudio Sacerdoti...	More work on inserting UnsafeCoerce in argument applications...	commit \| commitdiff \| tree
2012-09-19	Claudio Sacerdoti...	GHC.Prim.Any fixed	commit \| commitdiff \| tree
2012-09-04	Claudio Sacerdoti...	1. deriving (Show) no longer used because it fails...	commit \| commitdiff \| tree
2012-08-30	Claudio Sacerdoti...	Composite coercions are now extracted too.	commit \| commitdiff \| tree
2012-08-30	Claudio Sacerdoti...	Name mangling until separate extraction is implemented.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Code to make all global names in a file fresh.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Capitalization of variables bound in patterns fixed.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Fixed indentation, which is semantic in Haskell.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	(Part of previous two commits)	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	(Part of previous commit)	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Extraction is now integrated with the usual machinery...	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Top used also for fixes.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Match in types handled using top.	commit \| commitdiff \| tree
2012-08-29	Claudio Sacerdoti...	Match in types handled using Top.	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Match in classification of non-terms taken in account.	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Known bug fixed: the rhs of a match over a small singleton...	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Basics/logic.ma no longer raises exception.	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Bug fixed: when extracting pattern matching on singleton...	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Fixed pretty-printing of types of variables bound in...	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Patterns are now computed according to the extracted...	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	pattern arguments where printed in reverse order	commit \| commitdiff \| tree
2012-08-28	Claudio Sacerdoti...	Bug fixed: rhs in match were printed in wrong context.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Code for computing patterns the way Haskell likes them...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Fixed pretty-printing of mutual recursive stuff and...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	1. fixed pretty-printing of constructors, type variables...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Self contained now.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	1. added Skip to terms to maintain consistency between...	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Fixed left/right context distinction in inductive types.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Pretty printing of context (variable refreshing) fixed.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	size_of_type fixed and simplified	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	No pattern matching over empty types in Haskell	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Infos stored for inductive types.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Preliminary extraction of constructors.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	Added kind signatures to data declaration.	commit \| commitdiff \| tree
2012-08-27	Claudio Sacerdoti...	1. Dominic:	commit \| commitdiff \| tree
2012-08-22	Claudio Sacerdoti...	Preliminary work on (co)inductive types.	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Bug fixed: the context generated by l.h.s. binders...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Pretty printing of patterns done almost correctly.	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Tentative code for Fixpoint. Still to be completed.	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Path fixed.	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Code extraction branched.	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Temporary stuff to test code extraction. Running make...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	1. Implemented type inference for Fomega to extract...	commit \| commitdiff \| tree
2012-08-02	Claudio Sacerdoti...	Bugs fixed:	commit \| commitdiff \| tree
2012-08-01	Claudio Sacerdoti...	Bugs related to pretty printing of names fixed (capitalizati...	commit \| commitdiff \| tree
2012-08-01	Claudio Sacerdoti...	Tests for code extraction; to be moved elsewhere.	commit \| commitdiff \| tree
2012-08-01	Claudio Sacerdoti...	Bug fixed: Haskell forces capitalisation.	commit \| commitdiff \| tree
2012-08-01	Claudio Sacerdoti...	Begin of porting of code extraction to the new Matita.	commit \| commitdiff \| tree
2012-07-19	Claudio Sacerdoti...	One less warning.	commit \| commitdiff \| tree
2012-07-19	Claudio Sacerdoti...	Some debugging times exposed.	commit \| commitdiff \| tree
2012-07-19	Claudio Sacerdoti...	Major speed up improvement after every tactic application.	commit \| commitdiff \| tree
2012-06-29	Claudio Sacerdoti...	Bug fixed: arguments of a match are (no longer...)...	commit \| commitdiff \| tree
2012-06-11	Claudio Sacerdoti...	Reindented	commit \| commitdiff \| tree
2012-06-11	Claudio Sacerdoti...	New nohyps option for /demod/	commit \| commitdiff \| tree
2012-06-08	Claudio Sacerdoti...	New flags for demod:	commit \| commitdiff \| tree
2012-06-08	Claudio Sacerdoti...	Msg reporting via HLogger in the error window made...	commit \| commitdiff \| tree
2012-06-07	Claudio Sacerdoti...	Patch to avoid generating _inv_ind_recTX for X the...	commit \| commitdiff \| tree
2012-06-07	Claudio Sacerdoti...	Sys.Break no longer catched	commit \| commitdiff \| tree
2012-06-07	Claudio Sacerdoti...	New debugging switch in the interface.	commit \| commitdiff \| tree
2012-05-31	Claudio Sacerdoti...	Thanks to Guarrigue, code for Serializer functor simplified...	commit \| commitdiff \| tree
2012-05-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-05-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2012-05-17	Claudio Sacerdoti...	Efficient hashing used.	commit \| commitdiff \| tree
2012-05-17	Claudio Sacerdoti...	hash function exported	commit \| commitdiff \| tree
2012-05-17	Claudio Sacerdoti...	The lpo cache is now implemented as an hastbl for more...	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Added cache to lpo implementation.	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Orientation of equalities is now displayed.	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Orientation of equalities is now displayed.	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Removed duplicated notation and interaction with the...	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Compare was not compatible with eq!	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	New, faster implementation of lpo checked against old...	commit \| commitdiff \| tree
2012-05-16	Claudio Sacerdoti...	Added alias instance=1 to avoid interaction with the...	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	Pruning generalized from Vars to applied Vars.	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	Bug fixed in does_not_occur when a LetIn was found...	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	print => debug	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	Patch by Ferruccio that enables \top/\bot for False...	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	Divergence during indexing fixed: (? t = t') was not...	commit \| commitdiff \| tree
2012-05-15	Claudio Sacerdoti...	Sys.Break no longer caught during indexing	commit \| commitdiff \| tree
2012-05-10	Claudio Sacerdoti...	Patch to improve the pretty-printing of error messages.	commit \| commitdiff \| tree
next

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

RSS Atom