]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2008-04-23 Claudio Sacerdoti... Avoid other comparisons on universes using =.
2008-04-23 Claudio Sacerdoti... Avoid code duplication.
2008-04-23 Claudio Sacerdoti... Do NOT dare using Pervasives.compare on data structures...
2008-04-22 Enrico Tassioblivion ugraph everywhere outside the kernel
2008-04-22 Enrico Tassislow_implementation and some dead code removed
2008-04-22 Enrico Tassimore strict check by CSC, I miss it
2008-04-22 Enrico Tassifix cache comparison relaxed to URI and not REFERENCE
2008-04-22 Enrico Tassiadded a call to ppcontext in the case of appl, to ease...
2008-04-22 Enrico Tassiadded ppcontext
2008-04-22 Claudio Sacerdoti... Types for LetIns computed during parsing for Coq object...
2008-04-21 Claudio Sacerdoti... defn2.ma is to be used with part1a_inversion3
2008-04-21 Enrico Tassifix universe handling, newly encountered objects are...
2008-04-20 Claudio Sacerdoti... Alternative prove using just one induction/inversion...
2008-04-19 Enrico Tassibetter error message
2008-04-19 Enrico Tassi...
2008-04-19 Enrico Tassiimpredicative set work around
2008-04-19 Enrico Tassiimpredicative set work around
2008-04-19 Enrico Tassiassociativity of -> fixed
2008-04-19 Enrico Tassiancient graph regarding universes and trust=false,...
2008-04-19 Enrico Tassiextlib list_uniq instead of local copy
2008-04-19 Enrico Tassiranking function fixed: when graphs are collapsed one...
2008-04-19 Enrico Tassiadded flag to change Set into Type on the fly, that...
2008-04-19 Claudio Sacerdoti... oblivion_ugraph => empty_ugraph
2008-04-19 Claudio Sacerdoti... Added to flags to activate/disactivate pretty-printing...
2008-04-19 Claudio Sacerdoti... Uris must be stripped of their xpointers.
2008-04-18 Claudio Sacerdoti... Dead code removed.
2008-04-18 Claudio Sacerdoti... Inversion lemma for Forall.
2008-04-18 Enrico Tassiworkaround for Pi associativity
2008-04-18 Enrico Tassiworkaround for some Set/Type problems
2008-04-18 Enrico TassicicEnvironment refactoring with sound view of Coq`s...
2008-04-18 Enrico Tassiassertion was wrong, an object can contain a named...
2008-04-18 Enrico Tassigraph generation phase fixed
2008-04-18 Enrico TassiAppl case in is_really_smaller fixed as in the old...
2008-04-17 Enrico Tassiexample:
2008-04-17 Enrico Tassiadded a missing whd
2008-04-17 Enrico Tassinew calculation of recursive parameters in guarded...
2008-04-17 Enrico TassiTwo similar cases packed together
2008-04-17 Enrico Tassisome fixes for guardness conditions
2008-04-17 Enrico Tassiis_really_smaller in sync with old kernel, impossible...
2008-04-15 Claudio Sacerdoti... check_is_really_smaller simplified to consider that...
2008-04-15 Claudio Sacerdoti... 1. bug fixed: the context must be type-checked before...
2008-04-15 Enrico Tassiget_checked_fix -> get_checked_fixes
2008-04-15 Enrico Tassiadded comment
2008-04-15 Claudio Sacerdoti... added sample of guarded by in which coq is stronger
2008-04-15 Enrico Tassipositivity check fixed, a MutInd not applied (but with...
2008-04-15 Enrico Tassido not use an implicit but a sort as a neutral term...
2008-04-14 Enrico Tassiobjects are typechecked to ensure there is a graph...
2008-04-14 Enrico Tassileftno should be increased of the expnamedsubst, but...
2008-04-14 Enrico Tassibetter error message
2008-04-14 Enrico Tassisame_obj made more precise, fixed the order of the...
2008-04-14 Enrico Tassificed fixpoint cache usage for mutual fix
2008-04-14 Enrico Tassifixed positivity conditions
2008-04-14 Enrico Tassiadded mk_fix i j r that given an r of a fix generated...
2008-04-14 Enrico Tassipositivity condition was relying on the name declared...
2008-04-14 Enrico Tassiadded little optimization to not add twice the same arc
2008-04-11 Enrico Tassiquinck and untested implementation of positivity condit...
2008-04-11 Enrico Tassi...
2008-04-11 Enrico Tassiadded depndency of new kernel to metadata to allow...
2008-04-11 Enrico TassiFIXED bug, added assertion in case a universe inside...
2008-04-11 Enrico Tassiadded function to fresh types
2008-04-11 Enrico Tassicall Unshare.fresh_types
2008-04-11 Enrico Tassiload the graph of objects that depend on the ones reque...
2008-04-11 Enrico Tassiuse universe rank instead of Type0
2008-04-11 Enrico TassiType related failures fixed
2008-04-11 Enrico Tassibetter pp of objects
2008-04-11 Claudio Sacerdoti... Extracted code. The main executable is medium_tests...
2008-04-11 Enrico Tassiremoved useless file
2008-04-11 Enrico Tassifixed modules order
2008-04-11 Enrico Tassimore fix removed from types
2008-04-11 Enrico Tassimore fix removed from types in proofs
2008-04-11 Enrico Tassiwhen we build the elimination principle we fresh univer...
2008-04-11 Enrico Tassiadded a parameter to unshare universes
2008-04-11 Enrico TassiConversion of 2 lambdas was not requiring equality...
2008-04-11 Enrico Tassicontext of types built in the reverse order
2008-04-11 Enrico Tassiadded a simplify to prevent the generation of an ugly fix
2008-04-11 Enrico Tassiimplemented inductive and less parentheses
2008-04-10 Claudio Sacerdoti... The cache of objects is now used also for cofixpoints.
2008-04-10 Claudio Sacerdoti... New: cache of translated fixpoints (to avoid the genera...
2008-04-10 Claudio Sacerdoti... does_not_occur exported to be used in oCic2NCic
2008-04-09 Claudio Sacerdoti... Bug fixed: references to CoFix are CoFix, not Fix.
2008-04-09 Enrico Tassiprint unnamed variables as __n
2008-04-09 Enrico Tassiswitch off profilers
2008-04-09 Enrico Tassipp with parenthesis only when necessary and with some...
2008-04-09 Claudio Sacerdoti... ...
2008-04-09 Claudio Sacerdoti... Fixed serious bug that occurred only in the following...
2008-04-09 Enrico Tassibetter pp in Appl
2008-04-09 Enrico Tassibetter pp
2008-04-09 Enrico Tassipretty printer on steroids
2008-04-09 Claudio Sacerdoti... Added some "\n" here and there to the pretty-printing...
2008-04-09 Claudio Sacerdoti... Grave bug fixed: Ce that point to definitions were...
2008-04-09 Enrico Tassiadded profiling on/off
2008-04-09 Enrico Tassiinvalidate fixed
2008-04-09 Enrico Tassiallow to switch profiling on and off on the fly
2008-04-09 Enrico Tassiremoved two useless calls to the environment, one still...
2008-04-09 Enrico Tassi...
2008-04-08 Claudio Sacerdoti... Variables are no longer experted (cooking is now implem...
2008-04-08 Claudio Sacerdoti... Swapped arguments in error message.
2008-04-08 Claudio Sacerdoti... Variables having a body can occur in cooked terms and...
2008-04-08 Claudio Sacerdoti... Fix over the previous one: Var-LetIn abstractions shoul...
2008-04-08 Claudio Sacerdoti... Error message improved.
next