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

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

2014-02-27	Claudio Sacerdoti...	Porting of HOTT from Coq to Matita.	commit \| commitdiff \| tree
2013-12-02	Claudio Sacerdoti...	1. more bugs fixed	commit \| commitdiff \| tree
2013-12-02	Claudio Sacerdoti...	More progress.	commit \| commitdiff \| tree
2013-12-02	Claudio Sacerdoti...	Some progress in the correctness proof and a bug fixed.	commit \| commitdiff \| tree
2013-04-30	Claudio Sacerdoti...	Bumped to 0.99.2.	commit \| commitdiff \| tree
2013-04-30	Claudio Sacerdoti...	Missing include.	commit \| commitdiff \| tree
2013-04-30	Claudio Sacerdoti...	Old version dropped.	commit \| commitdiff \| tree
2013-04-08	Claudio Sacerdoti...	Patch by Paolo Tranquilli. It fixes the following problem...	commit \| commitdiff \| tree
2013-03-04	Claudio Sacerdoti...	Bug fixed: let-rec defined propositions are no longer...	commit \| commitdiff \| tree
2013-02-27	Claudio Sacerdoti...	Quick patch: the maxmeta is now pushed/popped when...	commit \| commitdiff \| tree
2013-02-27	Claudio Sacerdoti...	Quick patch: the maxmeta is now pushed/popped when...	commit \| commitdiff \| tree
2013-02-27	Claudio Sacerdoti...	Bug fixed: composite coercions were not extracted.	commit \| commitdiff \| tree
2013-02-27	Claudio Sacerdoti...	Bug fixed that reveals a new one: in case of inductive...	commit \| commitdiff \| tree
2013-02-27	Claudio Sacerdoti...	Ferruccio's removal of objects commented out because...	commit \| commitdiff \| tree
2013-02-05	Claudio Sacerdoti...	Bug fixed: .ml/.mli files were opened/closed even when...	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Bug fixed: "open X" were not printed in .mli because...	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Flushing needed before closing the channel.	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Improved exception handling.	commit \| commitdiff \| tree
2013-02-04	Claudio Sacerdoti...	Bug fixed in pretty printing of mutual inductive types.	commit \| commitdiff \| tree
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
next

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

RSS Atom