]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
lefts_ad_tys properly sorted, added some metasenv here and there,
[helm.git] / helm / software / components /
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-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-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 Enrico Tassiinsert comments of old tpechecker
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 TassiXXX this is the beginning of the metaocaml work XXX
2008-03-23 Ferruccio GuidicicNotationPp: fixed letin syntax (now typeless)
2008-03-20 Enrico Tassichanged auto_tac params type and all derivate tactics...
2008-03-20 Claudio Sacerdoti... End of patch for computation of LetIn types. Now types...
2008-03-19 Claudio Sacerdoti... Bug: types and terms pushed into the context must be...
2008-03-19 Claudio Sacerdoti... prerr_endline => debug_print
2008-03-19 Claudio Sacerdoti... prerr_endline => debug_print
2008-03-19 Claudio Sacerdoti... Number notation for Coq is back again, waiting for...
2008-03-19 Ferruccio GuidiProcedural : added some missing cases
2008-03-18 Ferruccio GuidiProcedural : tentative update to the new letin cic...
2008-03-13 Claudio Sacerdoti... :-(
2008-03-12 Claudio Sacerdoti... Almost always correct optimization: during unification...
2008-03-12 Enrico Tassifixed implicit
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-10 Claudio Sacerdoti... Bad hack to avoid failure of conversion (unfolding...
2008-03-10 Claudio Sacerdoti... ...
2008-03-10 Claudio Sacerdoti... Tactic reduce got rid of. Use normalize, instead.
2008-03-10 Claudio Sacerdoti... whd: ~delta=false now controls also zeta-reduction...
2008-03-10 Claudio Sacerdoti... An unimplemented case of clearbody is now implemented.
2008-03-10 Claudio Sacerdoti... check_metasenv_consistency:
2008-03-10 Claudio Sacerdoti... Debugging print removed.
2008-03-09 Claudio Sacerdoti... Added ad-hoc optimization for check_metasenv_consistenc...
2008-03-09 Claudio Sacerdoti... Performance improvement: let-ins should always be pushe...
2008-03-09 Claudio Sacerdoti... Potentially (and, at least sometimes, actually) big...
2008-03-09 Claudio Sacerdoti... Redundant check (because of an invariant) removed.
2008-03-06 Enrico Tassifix typo
2008-03-06 Enrico Tassiadded mkdir
2008-03-05 Enrico Tassiverbosity increased in case of error
2008-03-04 Ferruccio Guidicomponents/library: dotdothack removed
2008-02-26 Ferruccio GuidiI added some debugging information
2008-02-22 Ferruccio Guidi- added some options to matitadep: -stdout and -exclude
2008-02-21 Claudio Sacerdoti... A new very simple example for recursive functions....
2008-02-21 Claudio Sacerdoti... Avoid translating back recursive fixes to the same...
2008-02-21 Claudio Sacerdoti... Avoid application to 0 arguments.
2008-02-21 Claudio Sacerdoti... Better handling of exceptions.
2008-02-20 Enrico Tassisplat_args is now better understood and debugged: we...
2008-02-20 Enrico Tassiadded small test, fixed some bugs
2008-02-20 Enrico Tassimany fixed in translation functions
2008-02-19 Enrico Tassi...
2008-02-19 Enrico Tassisnapshot inverse tranformation
2008-02-19 Enrico Tassitransformation almost finisced, not tested
next