]> matita.cs.unibo.it Git - helm.git/history - matita/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
lazy equivalence for local environments is now defined
[helm.git] / matita / components /
2013-10-27 Ferruccio Guidi- lambdadelta: tentative definition of lazy equivalence... tree | commitdiff
2013-08-09 Ferruccio Guidi- matitadep: new option -t to list the unreferenced... tree | commitdiff
2013-07-27 Ferruccio Guidi- probe: critical bug fixed (all objects were deleted... tree | commitdiff
2013-07-26 Ferruccio Guidilambdadelta tree | commitdiff
2013-04-17 Wilmer RicciottiFixes a bug which caused Meta_not_found exceptions... tree | commitdiff
2013-04-09 Wilmer RicciottiFixes a bug that caused an assertion failure when no... tree | commitdiff
2013-03-20 Ferruccio Guidi- probe: recursive removal of empty directories tree | commitdiff
2013-03-16 Ferruccio Guidi- lambdadelta: last recursive part of preservation... tree | commitdiff
2013-03-13 Ferruccio Guidi- lambdadelta: third recursive part of preservation... tree | commitdiff
2013-03-10 Ferruccio Guidiwe removed a useless assertion that was forcing matita... tree | commitdiff
2013-03-04 Claudio Sacerdoti... Bug fixed: let-rec defined propositions are no longer... tree | commitdiff
2013-03-03 Ferruccio Guidi- lambdadelta: we removed focalized reduction from... tree | commitdiff
2013-02-27 Claudio Sacerdoti... Quick patch: the maxmeta is now pushed/popped when... tree | commitdiff
2013-02-27 Claudio Sacerdoti... Bug fixed: composite coercions were not extracted. tree | commitdiff
2013-02-27 Claudio Sacerdoti... Bug fixed that reveals a new one: in case of inductive... tree | commitdiff
2013-02-27 Claudio Sacerdoti... Ferruccio's removal of objects commented out because... tree | commitdiff
2013-02-25 Ferruccio Guidiwhen we serialize the contents of a .ma, we remove... tree | commitdiff
2013-02-24 Ferruccio Guidi- nUri : added Sets of uris for use in "probe" tree | commitdiff
2013-02-06 Ferruccio Guidi- lambdadelta: more service lemmas ... tree | commitdiff
2013-02-05 Ferruccio Guidisome missing files ... tree | commitdiff
2013-02-04 Claudio Sacerdoti... Bug fixed: "open X" were not printed in .mli because... tree | commitdiff
2013-02-04 Claudio Sacerdoti... Flushing needed before closing the channel. tree | commitdiff
2013-02-04 Claudio Sacerdoti... Improved exception handling. tree | commitdiff
2013-02-04 Claudio Sacerdoti... Bug fixed in pretty printing of mutual inductive types. tree | commitdiff
2013-02-04 Claudio Sacerdoti... Bug fixed: the indty can be typed with a Prod, not... tree | commitdiff
2013-02-04 Claudio Sacerdoti... Pretty printing of ocaml files slightly improved. tree | commitdiff
2013-02-04 Claudio Sacerdoti... Last known bug unrelated to names fixed: a fixpoint... tree | commitdiff
2013-02-02 Claudio Sacerdoti... Ooops, this completes the previous commit (ocaml extrac... tree | commitdiff
2013-02-02 Claudio Sacerdoti... Implementation of Ocaml extraction (largely ported... tree | commitdiff
2013-02-02 Claudio Sacerdoti... Identity change, improves readability. tree | commitdiff
2013-02-01 Ferruccio Guidi- ng_refiner: tree | commitdiff
2013-01-06 Ferruccio Guididependences update tree | commitdiff
2013-01-01 Ferruccio Guidi- probe: new application to compute some data on the... tree | commitdiff
2012-12-28 Ferruccio Guidixoa: change in naming convenctions for existential... tree | commitdiff
2012-12-06 Claudio Sacerdoti... Bug fixed: %n was badly failing (with Failure "nth... tree | commitdiff
2012-12-06 Wilmer RicciottiFixes a bug in NCicElim.pp (term -> ast conversion... tree | commitdiff
2012-11-09 Ferruccio Guidi- mac (ma count) tree | commitdiff
2012-10-19 Claudio Sacerdoti... One useless Obj.magic removed. tree | commitdiff
2012-10-08 Wilmer RicciottiDowngrades buggy destruct patch. tree | commitdiff
2012-10-05 Wilmer RicciottiRemoves debug prints that were left from last commit. tree | commitdiff
2012-10-05 Wilmer RicciottiThis patch allows generation of minimally dependent... tree | commitdiff
2012-09-19 Claudio Sacerdoti... More work on inserting UnsafeCoerce in argument applica... tree | commitdiff
2012-09-04 Claudio Sacerdoti... 1. deriving (Show) no longer used because it fails... tree | commitdiff
2012-08-30 Claudio Sacerdoti... Composite coercions are now extracted too. tree | commitdiff
2012-08-30 Claudio Sacerdoti... Name mangling until separate extraction is implemented. tree | commitdiff
2012-08-29 Claudio Sacerdoti... Code to make all global names in a file fresh. tree | commitdiff
2012-08-29 Claudio Sacerdoti... Capitalization of variables bound in patterns fixed. tree | commitdiff
2012-08-29 Claudio Sacerdoti... ... tree | commitdiff
2012-08-29 Claudio Sacerdoti... Fixed indentation, which is semantic in Haskell. tree | commitdiff
2012-08-29 Claudio Sacerdoti... (Part of previous two commits) tree | commitdiff
2012-08-29 Claudio Sacerdoti... (Part of previous commit) tree | commitdiff
2012-08-29 Claudio Sacerdoti... Extraction is now integrated with the usual machinery... tree | commitdiff
2012-08-29 Claudio Sacerdoti... Top used also for fixes. tree | commitdiff
2012-08-29 Claudio Sacerdoti... Match in types handled using Top. tree | commitdiff
2012-08-28 Claudio Sacerdoti... Dead code removed. tree | commitdiff
2012-08-28 Claudio Sacerdoti... Match in classification of non-terms taken in account. tree | commitdiff
2012-08-28 Claudio Sacerdoti... Known bug fixed: the rhs of a match over a small single... tree | commitdiff
2012-08-28 Claudio Sacerdoti... Basics/logic.ma no longer raises exception. tree | commitdiff
2012-08-28 Claudio Sacerdoti... Bug fixed: when extracting pattern matching on singleto... tree | commitdiff
2012-08-28 Claudio Sacerdoti... Fixed pretty-printing of types of variables bound in... tree | commitdiff
2012-08-28 Claudio Sacerdoti... Patterns are now computed according to the extracted... tree | commitdiff
2012-08-28 Claudio Sacerdoti... pattern arguments where printed in reverse order tree | commitdiff
2012-08-28 Claudio Sacerdoti... Bug fixed: rhs in match were printed in wrong context. tree | commitdiff
2012-08-27 Claudio Sacerdoti... Code for computing patterns the way Haskell likes them... tree | commitdiff
2012-08-27 Claudio Sacerdoti... Fixed pretty-printing of mutual recursive stuff and... tree | commitdiff
2012-08-27 Claudio Sacerdoti... 1. fixed pretty-printing of constructors, type variable... tree | commitdiff
2012-08-27 Claudio Sacerdoti... 1. added Skip to terms to maintain consistency between... tree | commitdiff
2012-08-27 Claudio Sacerdoti... Fixed left/right context distinction in inductive types. tree | commitdiff
2012-08-27 Claudio Sacerdoti... Pretty printing of context (variable refreshing) fixed. tree | commitdiff
2012-08-27 Claudio Sacerdoti... size_of_type fixed and simplified tree | commitdiff
2012-08-27 Claudio Sacerdoti... No pattern matching over empty types in Haskell tree | commitdiff
2012-08-27 Claudio Sacerdoti... Infos stored for inductive types. tree | commitdiff
2012-08-27 Claudio Sacerdoti... Preliminary extraction of constructors. tree | commitdiff
2012-08-27 Claudio Sacerdoti... Added kind signatures to data declaration. tree | commitdiff
2012-08-27 Claudio Sacerdoti... 1. Dominic: tree | commitdiff
2012-08-22 Claudio Sacerdoti... Preliminary work on (co)inductive types. tree | commitdiff
2012-08-02 Claudio Sacerdoti... Bug fixed: the context generated by l.h.s. binders... tree | commitdiff
2012-08-02 Claudio Sacerdoti... Pretty printing of patterns done almost correctly. tree | commitdiff
2012-08-02 Claudio Sacerdoti... Tentative code for Fixpoint. Still to be completed. tree | commitdiff
2012-08-02 Claudio Sacerdoti... Code extraction branched. tree | commitdiff
2012-08-02 Claudio Sacerdoti... 1. Implemented type inference for Fomega to extract... tree | commitdiff
2012-08-02 Claudio Sacerdoti... Bugs fixed: tree | commitdiff
2012-08-01 Claudio Sacerdoti... Bugs related to pretty printing of names fixed (capital... tree | commitdiff
2012-08-01 Claudio Sacerdoti... Bug fixed: Haskell forces capitalisation. tree | commitdiff
2012-08-01 Claudio Sacerdoti... Begin of porting of code extraction to the new Matita. tree | commitdiff
2012-07-19 Claudio Sacerdoti... One less warning. tree | commitdiff
2012-07-19 Claudio Sacerdoti... Some debugging times exposed. tree | commitdiff
2012-07-19 Claudio Sacerdoti... Major speed up improvement after every tactic application. tree | commitdiff
2012-06-29 Claudio Sacerdoti... Bug fixed: arguments of a match are (no longer...)... tree | commitdiff
2012-06-11 Claudio Sacerdoti... Reindented tree | commitdiff
2012-06-11 Claudio Sacerdoti... New nohyps option for /demod/ tree | commitdiff
2012-06-08 Claudio Sacerdoti... New flags for demod: tree | commitdiff
2012-06-07 Claudio Sacerdoti... Patch to avoid generating _inv_ind_recTX for X the... tree | commitdiff
2012-06-07 Claudio Sacerdoti... Sys.Break no longer catched tree | commitdiff
2012-06-07 Claudio Sacerdoti... New debugging switch in the interface. tree | commitdiff
2012-06-04 Ferruccio Guidi- lambda_delta: subject reduction for nativa type assig... tree | commitdiff
2012-05-31 Claudio Sacerdoti... Thanks to Guarrigue, code for Serializer functor simpli... tree | commitdiff
2012-05-30 Ferruccio Guidi- nDestructTac: Sys.break handled in two places tree | commitdiff
2012-05-17 Ferruccio Guididepenences fixup tree | commitdiff
2012-05-17 Claudio Sacerdoti... ... tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.