]> matita.cs.unibo.it Git - helm.git/history - helm
Variables having a body can occur in cooked terms and must be delta-expanded
[helm.git] / helm /
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...
2008-03-22 Enrico Tassimoved dama/ and dama_didactic/ in contribs/dama/
2008-03-22 Enrico Tassifreescale moved under contribs. contribs made relocatable
2008-03-20 Claudio Sacerdoti... New syntax for auto-related tactics and conclude/obtain.
2008-03-20 Claudio Sacerdoti... Script fixed (it did not compile due to a mistake befor...
2008-03-20 Ferruccio GuidiBase-2 is not compiling properly and is excluded for now
2008-03-20 Enrico Tassichanged auto_tac params type and all derivate tactics...
2008-03-20 Enrico Tassinew semantics for 'by t'
2008-03-20 Enrico Tassiremoved pointless test
2008-03-20 Enrico TassiI believe that auto paramodulation does not try to
2008-03-20 Enrico Tassiadded library option to auto
2008-03-20 Enrico Tassiletins are no more unfolded, we do that by hand
2008-03-20 Enrico Tassiletin are no longer unfolded thus coercions not propaga...
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... -debug improved
2008-03-19 Claudio Sacerdoti... ...
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 Claudio Sacerdoti... Files committed by Enrico (a mistake, I suppose) removed.
2008-03-19 Ferruccio GuidiProcedural : added some missing cases
2008-03-18 Ferruccio GuidiLAMBDA-TYPES: level 2 dependences are now correct,...
2008-03-18 Ferruccio GuidiProcedural : tentative update to the new letin cic...
2008-03-14 Claudio Sacerdoti... Tests enabled again.
2008-03-13 Claudio Sacerdoti... :-(
2008-03-13 Claudio Sacerdoti... New version of freescale:
2008-03-12 Claudio Sacerdoti... Problem solved (was: apply needed an argument to avoid...
2008-03-12 Claudio Sacerdoti... Almost always correct optimization: during unification...
2008-03-12 Enrico Tassifixed implicit
2008-03-12 Andrea AspertiNuova dimostrazione riflessiva di le_to_Bertrand.
2008-03-12 Enrico Tassiif -debug is specified do not catch all exceptions
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-10 Enrico Tassifixed wrong dependencies in debian package reported...
2008-03-10 Claudio Sacerdoti... Bad hack to avoid failure of conversion (unfolding...
2008-03-10 Claudio Sacerdoti... ...
2008-03-10 Claudio Sacerdoti... Scripts fixed because of:
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... Example query fixed.
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... Scripts fixed. They were broken since the change to...
2008-03-09 Ferruccio GuidiLAMBDA-TYPES: some more generation lemmas and some...
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 Tassi* please let the library in shape *
2008-03-06 Enrico Tassifixed
2008-03-06 Enrico Tassiskipped freescale and dama_didactic
2008-03-06 Enrico Tassifixed deps
2008-03-06 Enrico Tassireworked freescale stuff to put \m as a left parameter
2008-03-06 Enrico Tassino more assembly/ to skip
2008-03-06 Enrico Tassifix typo
2008-03-06 Enrico Tassiadded mkdir
2008-03-06 Enrico Tassi...
2008-03-05 Ferruccio Guidisome corrections and additions
2008-03-05 Enrico Tassifrom now on, export MATITA_EXTRACT=true to extract
2008-03-05 Enrico Tassiverbosity increased in case of error
2008-03-04 Ferruccio Guidicomponents/library: dotdothack removed
2008-03-04 Claudio Sacerdoti... New syntax for patterns.
2008-03-04 Claudio Sacerdoti... prodT ==> prod
2008-03-04 Claudio Sacerdoti... A) New version.
2008-02-29 Ferruccio Guidiwe added the classic substitution function
2008-02-28 Enrico Tassifirs attempt to compile with ocamlbuild
2008-02-27 Wilmer Ricciottithe proof of bertrand's conjecture is now complete
2008-02-26 Ferruccio GuidiI added some debugging information
2008-02-26 Ferruccio Guidiadded MATITAOPTIONS -onepass as for LAMBDA-TYPES
2008-02-26 Ferruccio GuidiLAMBDA-TYPES: added wf3 (legal context predicate);
2008-02-24 Ferruccio Guidi$(H) added :)
2008-02-24 Ferruccio GuidiLAMBDA-TYPES: dependences calculation improved
2008-02-23 Ferruccio GuidiLAMBDA-TYPES:
2008-02-22 Ferruccio Guidi- added some options to matitadep: -stdout and -exclude
2008-02-22 Wilmer Ricciottisieve of erathostene (proof of soundness almost done)
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-21 Ferruccio Guidisvn:ignores fixed
2008-02-20 Ferruccio Guidi-onepass option removed from Makefile to comile Base...
2008-02-20 Ferruccio GuidiLambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
2008-02-20 Enrico Tassisplat_args is now better understood and debugged: we...
next