]> matita.cs.unibo.it Git - helm.git/history - matita/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
more porting to machines that can move without writing
[helm.git] / matita / components /
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
2012-05-17 Claudio Sacerdoti... ... tree | commitdiff
2012-05-17 Claudio Sacerdoti... Efficient hashing used. tree | commitdiff
2012-05-17 Claudio Sacerdoti... hash function exported tree | commitdiff
2012-05-17 Claudio Sacerdoti... The lpo cache is now implemented as an hastbl for more... tree | commitdiff
2012-05-16 Claudio Sacerdoti... Added cache to lpo implementation. tree | commitdiff
2012-05-16 Claudio Sacerdoti... Orientation of equalities is now displayed. tree | commitdiff
2012-05-16 Claudio Sacerdoti... Orientation of equalities is now displayed. tree | commitdiff
2012-05-16 Claudio Sacerdoti... Compare was not compatible with eq! tree | commitdiff
2012-05-16 Claudio Sacerdoti... New, faster implementation of lpo checked against old... tree | commitdiff
2012-05-16 Andrea AspertiNew implementation of lpo (the previous one was sometim... tree | commitdiff
2012-05-15 Claudio Sacerdoti... Pruning generalized from Vars to applied Vars. tree | commitdiff
2012-05-15 Claudio Sacerdoti... Bug fixed in does_not_occur when a LetIn was found... tree | commitdiff
2012-05-15 Claudio Sacerdoti... print => debug tree | commitdiff
2012-05-15 Claudio Sacerdoti... Divergence during indexing fixed: (? t = t') was not... tree | commitdiff
2012-05-15 Claudio Sacerdoti... Sys.Break no longer caught during indexing tree | commitdiff
2012-05-10 Claudio Sacerdoti... Patch to improve the pretty-printing of error messages. tree | commitdiff
2012-05-10 Claudio Sacerdoti... Sys.Break no longer captured in two places. tree | commitdiff
2012-05-03 Claudio Sacerdoti... Speed up: moved a #ppterm inside the lazy it belongs to. tree | commitdiff
2012-03-09 Ferruccio Guidi- lambda_delta: morew propertie in context-sensitive... tree | commitdiff
2012-03-06 Claudio Sacerdoti... Forward compatibility with new releases of Camlp5. tree | commitdiff
2012-03-06 Claudio Sacerdoti... Workaround for a BSD bug (submitted by Boender). tree | commitdiff
2012-01-27 Wilmer RicciottiFixes a bug in is_flexible (when checking a meta in... tree | commitdiff
2012-01-27 Claudio Sacerdoti... Better error messages. tree | commitdiff
2012-01-23 Wilmer RicciottiInversion principles generation falls back to cases... tree | commitdiff
2012-01-12 Wilmer RicciottiImproves the presentation of hypotheses in the goal... tree | commitdiff
2012-01-11 Wilmer RicciottiFixes r11788 (partial, thus broken commit). tree | commitdiff
2012-01-10 Ferruccio Guidiunpatched version for the new CamplP5 tree | commitdiff
2012-01-10 Ferruccio Guidipatched version for old CamlP5 tree | commitdiff
2012-01-10 Wilmer RicciottiBugfix: NCicUnification.could_reduce now performs whd... tree | commitdiff
2012-01-07 Ferruccio Guidilambda_delta: global environments handling: redefined... tree | commitdiff
2011-12-16 Andrea AspertiIn case paramodulation fails we apply unit equalities. tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.