]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
removed dummy rewrite
[helm.git] / helm / software / components /
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
2008-02-19 Ferruccio Guidinow inline "file.ma" is allowed.
2008-02-19 Enrico Tassiinitial steps of convertibility
2008-02-18 Enrico Tassisome bits of reduction, reusing psubst
2008-02-13 Enrico Tassiconversion half inplemented
2008-02-13 Enrico Tassireordered cases
2008-02-13 Enrico Tassireorganization of sources
2008-02-13 Enrico Tassisubstituion and lifting implemented
2008-02-13 Enrico Tassifactorized common components of objects
2008-02-13 Enrico Tassiadded Local pragma, moved leftno and inductive into...
2008-02-13 Enrico Tassiadded leftno to indtypes, better indentation and comments
2008-02-12 Enrico TassinCic almost finished
2008-02-12 Enrico Tassiallow to use "../foo/bar.ma" as a path for the include...
2008-02-08 Claudio Sacerdoti... Bug fixed in generation of elimination principles of...
2008-02-05 Enrico Tassicic defined (half)
2008-02-05 Enrico Tassireindent
2008-02-05 Enrico Tassioldenv2newenv cache
2008-02-05 Enrico Tassiuri and references(uri)
2008-02-05 Enrico Tassiuri -> reference (2)
2008-02-05 Enrico Tassiuri -> reference
2008-01-31 Wilmer RicciottiOne Obj.magic implemented, trust changed to false.
2008-01-31 Wilmer RicciottiTransformation back and forth between old and new repre...
2008-01-31 Enrico Tassisnapshot
2008-01-31 Enrico Tassinew uri defined
2008-01-31 Enrico Tassisnapshot]
2008-01-30 Enrico Tassiadded meta for the new kernel
2008-01-30 Enrico Tassistub functions to make all compile
2008-01-30 Enrico Tassibasic organization of the new kernel
2008-01-22 Enrico Tassi...
2008-01-14 Enrico Tassiadded some doc
2008-01-14 Enrico Tassibetter parsing of the root file
2008-01-11 Enrico Tassiadded a warning when a file is not compiled cause its...
2008-01-11 Enrico TassiMake does not even try to build files that would be...
2008-01-11 Enrico Tassicache for mtime of files is not polluted with None...
2008-01-11 Enrico TassiMake was caching too much, thus some targets were not...
2008-01-10 Enrico TassiBIG FAT WARNING: DEVELOPMENTS DIE HERE
2007-12-04 Claudio Sacerdoti... Even if the error is not localized, it was not a good...
2007-12-04 Claudio Sacerdoti... Some terms are not localized from the very beginning :-(
2007-12-04 Claudio Sacerdoti... One more error localized. But the code is really ugly...
next