]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2008-04-08 Claudio Sacerdoti... j off by one in error message
2008-04-08 Claudio Sacerdoti... fix_outty partially fixed: missing lifts in args and ens
2008-04-08 Claudio Sacerdoti... fix_outty fixed in order to perform eta-expansion when...
2008-04-08 Enrico Tassiadded simplify to avoid ugly proofterm
2008-04-07 Claudio Sacerdoti... Tentative (and bad!) fix of outtypes in non-dependent...
2008-04-07 Claudio Sacerdoti... Cooking discriminated into cooking in types (using...
2008-04-07 Claudio Sacerdoti... Pretty-printing of definitions fixed.
2008-04-07 Claudio Sacerdoti... Cooking implemented (not tested yet).
2008-04-07 Claudio Sacerdoti... Reports improved.
2008-04-07 Claudio Sacerdoti... Debugging code fixed.
2008-04-07 Enrico Tassiadded invalidate to clear the cache and ease the compar...
2008-04-07 Enrico Tassicommented out uris of objs that do not compile properly
2008-04-07 Enrico Tassiadded comparison with old kernel
2008-04-07 Enrico Tassifixed error message for eat prods
2008-04-07 Enrico Tassiinvalidate
2008-04-07 Enrico Tassiuris relative to axioms are translated in the right way
2008-04-07 Enrico Tassiadded invalidate
2008-04-07 Enrico Tassiadded preliminary checks for indtys
2008-04-07 Enrico Tassicall get_obj instead of get_cooked_obj ~trust:false
2008-04-07 Enrico Tassiadded case of const and axiom
2008-04-07 Enrico Tassiadded # to comment
2008-04-07 Enrico Tassibetter printings
2008-04-07 Enrico Tassithe explicit type in a LetIn must be typecheckd before...
2008-04-07 Enrico Tassiopt compilation enabled, removed some pps, check has...
2008-04-07 Enrico Tassilefts_ad_tys properly sorted, added some metasenv here...
2008-04-07 Enrico Tassilefts_and_tys was tys@lefts, CSC claims it was working...
2008-04-07 Enrico Tassiadded a list of uris to ease debugging
2008-04-07 Enrico Tassiprint the excpetion and raise it again, seems to produc...
2008-04-07 Enrico Tassinew constants have depth = max_int insted of 0 so that...
2008-04-07 Enrico Tassioff by one in calling count_from
2008-04-07 Enrico Tassifixed bug in translating Fix, recno was not properly...
2008-04-07 Enrico Tassiadded a pretty printing of the new object and use argv...
2008-04-07 Enrico Tassicontext, metasenv and subst made mandatory in CicPp
2008-04-07 Enrico Tassiguarded by has a nice error message
2008-04-07 Enrico Tassireference type made private, added mk_constructor to...
2008-04-04 Enrico Tassisome debug printings
2008-04-04 Enrico Tassiadded to the cache a boolean to state if the object is
2008-04-04 Enrico Tassifix
2008-04-04 Enrico Tassitoday it seems that the substituted should be lifted...
2008-04-04 Enrico Tassiadded ppobj
2008-04-04 Enrico Tassitype_of_constant was retunrning the type of the wrong...
2008-04-04 Enrico Tassifixed list.nth and added some paretheses
2008-04-04 Enrico Tassiadded some printings and catched more exceptions
2008-04-04 Enrico Tassiremoved useless printing
2008-04-04 Enrico Tassiiterator map was mapping Lambdas to Prods!!!
2008-04-04 Enrico Tassidebugging started
2008-04-04 Enrico Tassitype of constant ported
2008-04-04 Enrico Tassiadded add_obj to store objects in the environment,...
2008-04-04 Enrico Tassilogger added
2008-04-04 Enrico Tassiadded get_obj in nCicEnvironment that returns an object...
2008-04-04 Enrico Tassiindentation fixed
2008-04-04 Enrico Tassireturns_a_counductive implemented
2008-04-04 Enrico Tassitype_of_branch ported and optimized to not lift the...
2008-04-04 Enrico Tassiis_really_smaller ported, still to understand the case...
2008-04-03 Enrico Tassidebujin implemented with the map recursor
2008-04-03 Enrico Tassibug found rewriting the kernel backported: n instead...
2008-04-03 Enrico Tassinon debruijned constructor may be useless elswere,...
2008-04-03 Enrico Tassiguarded_by_destructor ported, many auxiliary functions...
2008-04-03 Enrico Tassiremoved FSF banner
2008-04-03 Enrico Tassiadded ugly test showing many many bugs in the current...
2008-04-02 Enrico Tassiadded slim version of does_not_occur
2008-04-02 Enrico Tassiadded translation of Set to Type0 (avoid warning)
2008-04-02 Enrico Tassifixes backported from the new kernel
2008-04-02 Enrico Tassiremoved dummy rewrite
2008-04-02 Enrico Tassiremoved dummy rewrite
2008-04-02 Enrico Tassiremoved dummy rewrites
2008-04-02 Enrico Tassifixed according to the new rewrite semantics (fails...
2008-04-02 Enrico Tassifixed depends after the removal of Fsub
2008-04-01 Enrico Tassibetter check for progress
2008-04-01 Claudio Sacerdoti... typeof_obj0 implemented
2008-04-01 Claudio Sacerdoti... 1) added get_checked_indtys that returns the whole...
2008-04-01 Enrico Tassiprogress made better, still not perfect
2008-04-01 Enrico Tassiadded to rewrite a check to effectively do something...
2008-04-01 Enrico Tassiadded some comments, but the samentics of many function...
2008-04-01 Enrico Tassiadded set_ppterm
2008-03-31 Claudio Sacerdoti... Automatic generation of elimination and inversion princ...
2008-03-31 Claudio Sacerdoti... Large amount of duplicated code (still in comments...
2008-03-31 Claudio Sacerdoti... 1) Impredicative sort "Set" removed everywhere.
2008-03-31 Claudio Sacerdoti... 1) more sharing everywhere in NCicSubstitution
2008-03-27 Enrico Tassimore cases of the type checker honoured, still missing...
2008-03-27 Enrico Tassiadded is_closed to nCicUtils.
2008-03-27 Enrico Tassimoved psubst and list to the new iterators, result...
2008-03-27 Enrico Tassiadded iterators over NCic terms
2008-03-27 Enrico Tassiremoved FSF header
2008-03-27 Wilmer RicciottiUpdated depedencies.
2008-03-27 Enrico Tassiinsert comments of old tpechecker
2008-03-26 Wilmer RicciottiReorganization of list library (step 1)
2008-03-25 Enrico Tassinew are_convertible and head_beta_reduce
2008-03-25 Enrico Tassicontext for fixpoint body created in the hopefully...
2008-03-25 Enrico Tassiported to the Cic LetIn with explicit type
2008-03-25 Enrico Tassithis patch is a shit, the part that fixes the heuristic...
2008-03-25 Enrico Tassifix with m (to be optimized) are rewritten such that...
2008-03-25 Enrico Tassivery very interesting hack
2008-03-25 Wilmer Ricciottismall update
2008-03-25 Enrico Tassiargument of type mcu_type always abstracted first
2008-03-25 Enrico TassiXXX this is the beginning of the metaocaml work XXX
2008-03-23 Enrico TassiFsub moved in contribs
2008-03-23 Ferruccio GuidicicNotationPp: fixed letin syntax (now typeless)
2008-03-22 Enrico Tassisince many stuff is under contrib, we need to ignore...
2008-03-22 Enrico Tassilibrary_auto moved inside contrib, still not ported...
next