]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Dead code removed.
[helm.git] / helm / software / components /
2008-04-18 Enrico Tassiworkaround for Pi associativity tree | commitdiff
2008-04-18 Enrico Tassiworkaround for some Set/Type problems tree | commitdiff
2008-04-18 Enrico TassicicEnvironment refactoring with sound view of Coq`s... tree | commitdiff
2008-04-18 Enrico Tassiassertion was wrong, an object can contain a named... tree | commitdiff
2008-04-18 Enrico Tassigraph generation phase fixed tree | commitdiff
2008-04-18 Enrico TassiAppl case in is_really_smaller fixed as in the old... tree | commitdiff
2008-04-17 Enrico Tassiexample: tree | commitdiff
2008-04-17 Enrico Tassiadded a missing whd tree | commitdiff
2008-04-17 Enrico Tassinew calculation of recursive parameters in guarded... tree | commitdiff
2008-04-17 Enrico TassiTwo similar cases packed together tree | commitdiff
2008-04-17 Enrico Tassisome fixes for guardness conditions tree | commitdiff
2008-04-17 Enrico Tassiis_really_smaller in sync with old kernel, impossible... tree | commitdiff
2008-04-15 Claudio Sacerdoti... check_is_really_smaller simplified to consider that... tree | commitdiff
2008-04-15 Claudio Sacerdoti... 1. bug fixed: the context must be type-checked before... tree | commitdiff
2008-04-15 Enrico Tassiget_checked_fix -> get_checked_fixes tree | commitdiff
2008-04-15 Enrico Tassiadded comment tree | commitdiff
2008-04-15 Enrico Tassipositivity check fixed, a MutInd not applied (but with... tree | commitdiff
2008-04-15 Enrico Tassido not use an implicit but a sort as a neutral term... tree | commitdiff
2008-04-14 Enrico Tassiobjects are typechecked to ensure there is a graph... tree | commitdiff
2008-04-14 Enrico Tassileftno should be increased of the expnamedsubst, but... tree | commitdiff
2008-04-14 Enrico Tassibetter error message tree | commitdiff
2008-04-14 Enrico Tassisame_obj made more precise, fixed the order of the... tree | commitdiff
2008-04-14 Enrico Tassificed fixpoint cache usage for mutual fix tree | commitdiff
2008-04-14 Enrico Tassifixed positivity conditions tree | commitdiff
2008-04-14 Enrico Tassiadded mk_fix i j r that given an r of a fix generated... tree | commitdiff
2008-04-14 Enrico Tassipositivity condition was relying on the name declared... tree | commitdiff
2008-04-14 Enrico Tassiadded little optimization to not add twice the same arc tree | commitdiff
2008-04-11 Enrico Tassiquinck and untested implementation of positivity condit... tree | commitdiff
2008-04-11 Enrico Tassi... tree | commitdiff
2008-04-11 Enrico Tassiadded depndency of new kernel to metadata to allow... tree | commitdiff
2008-04-11 Enrico TassiFIXED bug, added assertion in case a universe inside... tree | commitdiff
2008-04-11 Enrico Tassiadded function to fresh types tree | commitdiff
2008-04-11 Enrico Tassicall Unshare.fresh_types tree | commitdiff
2008-04-11 Enrico Tassiload the graph of objects that depend on the ones reque... tree | commitdiff
2008-04-11 Enrico Tassiuse universe rank instead of Type0 tree | commitdiff
2008-04-11 Enrico TassiType related failures fixed tree | commitdiff
2008-04-11 Enrico Tassibetter pp of objects tree | commitdiff
2008-04-11 Enrico Tassiremoved useless file tree | commitdiff
2008-04-11 Enrico Tassifixed modules order tree | commitdiff
2008-04-11 Enrico Tassiwhen we build the elimination principle we fresh univer... tree | commitdiff
2008-04-11 Enrico Tassiadded a parameter to unshare universes tree | commitdiff
2008-04-11 Enrico TassiConversion of 2 lambdas was not requiring equality... tree | commitdiff
2008-04-11 Enrico Tassicontext of types built in the reverse order tree | commitdiff
2008-04-11 Enrico Tassiimplemented inductive and less parentheses tree | commitdiff
2008-04-10 Claudio Sacerdoti... The cache of objects is now used also for cofixpoints. tree | commitdiff
2008-04-10 Claudio Sacerdoti... New: cache of translated fixpoints (to avoid the genera... tree | commitdiff
2008-04-10 Claudio Sacerdoti... does_not_occur exported to be used in oCic2NCic tree | commitdiff
2008-04-09 Claudio Sacerdoti... Bug fixed: references to CoFix are CoFix, not Fix. tree | commitdiff
2008-04-09 Enrico Tassiprint unnamed variables as __n tree | commitdiff
2008-04-09 Enrico Tassiswitch off profilers tree | commitdiff
2008-04-09 Enrico Tassipp with parenthesis only when necessary and with some... tree | commitdiff
2008-04-09 Claudio Sacerdoti... ... tree | commitdiff
2008-04-09 Claudio Sacerdoti... Fixed serious bug that occurred only in the following... tree | commitdiff
2008-04-09 Enrico Tassibetter pp in Appl tree | commitdiff
2008-04-09 Enrico Tassibetter pp tree | commitdiff
2008-04-09 Enrico Tassipretty printer on steroids tree | commitdiff
2008-04-09 Claudio Sacerdoti... Added some "\n" here and there to the pretty-printing... tree | commitdiff
2008-04-09 Claudio Sacerdoti... Grave bug fixed: Ce that point to definitions were... tree | commitdiff
2008-04-09 Enrico Tassiadded profiling on/off tree | commitdiff
2008-04-09 Enrico Tassiinvalidate fixed tree | commitdiff
2008-04-09 Enrico Tassiallow to switch profiling on and off on the fly tree | commitdiff
2008-04-09 Enrico Tassiremoved two useless calls to the environment, one still... tree | commitdiff
2008-04-09 Enrico Tassi... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Variables are no longer experted (cooking is now implem... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Swapped arguments in error message. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Variables having a body can occur in cooked terms and... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Fix over the previous one: Var-LetIn abstractions shoul... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Error message improved. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Cooking w.r.t. variables with bodies is now implemented... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Fix name capture in cofix. tree | commitdiff
2008-04-08 Claudio Sacerdoti... To test the translation. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Name capture fixed. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Improved error messages in place of "sort elimination... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Seed reset before each convert_obj. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Use seed to avoid further name clashes. tree | commitdiff
2008-04-08 Claudio Sacerdoti... ... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Incredible, but true! Our name mangling clashed with... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Cooked objects are no longer well typed in the uncooked... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Improved eat_prods error message (at the cost of passin... tree | commitdiff
2008-04-08 Claudio Sacerdoti... The old kernel does not accept ens whose order is diffe... tree | commitdiff
2008-04-08 Claudio Sacerdoti... Bad alpha-conversion by Enrico fixed. tree | commitdiff
2008-04-08 Claudio Sacerdoti... Bug fixed: the ens need not be ordered w.r.t. the decla... tree | commitdiff
2008-04-08 Claudio Sacerdoti... j off by one in error message tree | commitdiff
2008-04-08 Claudio Sacerdoti... fix_outty partially fixed: missing lifts in args and ens tree | commitdiff
2008-04-08 Claudio Sacerdoti... fix_outty fixed in order to perform eta-expansion when... tree | commitdiff
2008-04-07 Claudio Sacerdoti... Tentative (and bad!) fix of outtypes in non-dependent... tree | commitdiff
2008-04-07 Claudio Sacerdoti... Cooking discriminated into cooking in types (using... tree | commitdiff
2008-04-07 Claudio Sacerdoti... Pretty-printing of definitions fixed. tree | commitdiff
2008-04-07 Claudio Sacerdoti... Cooking implemented (not tested yet). tree | commitdiff
2008-04-07 Claudio Sacerdoti... Reports improved. tree | commitdiff
2008-04-07 Claudio Sacerdoti... Debugging code fixed. tree | commitdiff
2008-04-07 Enrico Tassiadded invalidate to clear the cache and ease the compar... tree | commitdiff
2008-04-07 Enrico Tassicommented out uris of objs that do not compile properly tree | commitdiff
2008-04-07 Enrico Tassiadded comparison with old kernel tree | commitdiff
2008-04-07 Enrico Tassifixed error message for eat prods tree | commitdiff
2008-04-07 Enrico Tassiinvalidate tree | commitdiff
2008-04-07 Enrico Tassiuris relative to axioms are translated in the right way tree | commitdiff
2008-04-07 Enrico Tassiadded invalidate tree | commitdiff
2008-04-07 Enrico Tassiadded preliminary checks for indtys tree | commitdiff
2008-04-07 Enrico Tassicall get_obj instead of get_cooked_obj ~trust:false tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.