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

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

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
2012-05-10	Claudio Sacerdoti...	Sys.Break no longer captured in two places.	commit \| commitdiff \| tree
2012-05-04	Claudio Sacerdoti...	(no commit message)	commit \| commitdiff \| tree
2012-05-04	Claudio Sacerdoti...	(no commit message)	commit \| commitdiff \| tree
2012-05-03	Claudio Sacerdoti...	Speed up: moved a #ppterm inside the lazy it belongs to.	commit \| commitdiff \| tree
2012-04-17	Claudio Sacerdoti...	Fixed w.r.t. new yelp.	commit \| commitdiff \| tree
2012-03-09	Claudio Sacerdoti...	Fixes bug where switching to a new tab the slider is...	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	Forward compatibility with new releases of Camlp5.	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	Workaround for a BSD bug (submitted by Boender).	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	Bug fixed: horizontal scrolling now works correctly...	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	MAJOR SPEED UP. The previous implementation of scrolling...	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	Minor speed up in the code.	commit \| commitdiff \| tree
2012-03-06	Claudio Sacerdoti...	Major speed-up improvement. Adding one callback per...	commit \| commitdiff \| tree
2012-01-31	Claudio Sacerdoti...	Notation for destructuring let-in for triples fixed.	commit \| commitdiff \| tree
2012-01-27	Claudio Sacerdoti...	Better error messages.	commit \| commitdiff \| tree
2011-12-14	Claudio Sacerdoti...	More stuff from CerCo to the standard library.	commit \| commitdiff \| tree
2011-12-14	Claudio Sacerdoti...	Some more lemmas from CerCo.	commit \| commitdiff \| tree
2011-12-14	Claudio Sacerdoti...	1) Notation for dependent pairs differentiated from...	commit \| commitdiff \| tree
2011-12-13	Claudio Sacerdoti...	Dependent pairs (i.e. Sigma types in Type[0]) are back...	commit \| commitdiff \| tree
2011-12-13	Claudio Sacerdoti...	1) PSig and Sig merged into a single Sigma type in...	commit \| commitdiff \| tree
2011-12-13	Claudio Sacerdoti...	inject/eject replaced by mk_Sig/pi1.	commit \| commitdiff \| tree
2011-12-13	Claudio Sacerdoti...	1) New file russell with the coercions to activate...	commit \| commitdiff \| tree
2011-12-13	Claudio Sacerdoti...	More stuff integrated from CerCo on sigma types (that...	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	pair => mk_Prod (one more was left in notation)	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	precedence level of if-then-else fixed	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	Added elimination principles for destructuring let...	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	Some integrations from CerCo. In particular:	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	Pairs are now records.	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	Parentheses are now needed. I do not know why and when...	commit \| commitdiff \| tree
2011-12-12	Claudio Sacerdoti...	Re-Ported to	commit \| commitdiff \| tree
next

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

RSS Atom