]> matita.cs.unibo.it Git - helm.git/history - matita/components/ng_kernel
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
- local environment refinement for the first recursive lemma on validity preservation
[helm.git] / matita / components / ng_kernel /
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... 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... 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... Major speed up improvement after every tactic application. tree | commitdiff
2012-06-11 Claudio Sacerdoti... Reindented tree | commitdiff
2012-05-17 Claudio Sacerdoti... hash function exported tree | commitdiff
2012-05-15 Claudio Sacerdoti... Bug fixed in does_not_occur when a LetIn was found... tree | commitdiff
2012-05-10 Claudio Sacerdoti... Patch to improve the pretty-printing of error messages. tree | commitdiff
2012-01-07 Ferruccio Guidilambda_delta: global environments handling: redefined... tree | commitdiff
2011-11-24 Ferruccio Guidi- now destruct tries to clear the replaced variables... tree | commitdiff
2011-11-18 Claudio Sacerdoti... * Almost ready for release 0.99.1. tree | commitdiff
2011-10-18 Wilmer RicciottiChanges in "destruct" tactic (allowing performance... tree | commitdiff
2011-07-15 Claudio Sacerdoti... Bug fixed: when we try to add an object and it is not... tree | commitdiff
2011-06-01 Claudio Sacerdoti... assert false removed tree | commitdiff
2011-03-14 Ferruccio Guididependences fix tree | commitdiff
2011-01-11 Claudio Sacerdoti... HUGE COMMIT: tree | commitdiff
2010-12-23 Andrea Asperti1. bug in addition of universe constraints fixed: the... tree | commitdiff
2010-12-02 Claudio Sacerdoti... [ porting from CerCo's Matita ] tree | commitdiff
2010-11-19 Andrea AspertiImplementation of proof irrelevance finished. tree | commitdiff
2010-10-26 Andrea Asperticic module removed (RIP) tree | commitdiff
2010-10-07 Andrea Asperti- cic_exportation, cic_acic, acic_content (only parts... tree | commitdiff
2010-09-30 Enrico Tassisync with stable: tree | commitdiff
2010-09-30 Claudio Sacerdoti... Stuff moved from old Matita. tree | commitdiff
Unnamed repository; edit this file 'description' to name the repository.