| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | Number notation for Coq is back again, waiting for... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | Files committed by Enrico (a mistake, I suppose) removed. |
tree | commitdiff |
| 2008-03-19 |
Ferruccio Guidi | Procedural : added some missing cases |
tree | commitdiff |
| 2008-03-18 |
Ferruccio Guidi | LAMBDA-TYPES: level 2 dependences are now correct,... |
tree | commitdiff |
| 2008-03-18 |
Ferruccio Guidi | Procedural : tentative update to the new letin cic... |
tree | commitdiff |
| 2008-03-14 |
Claudio Sacerdoti... | Tests enabled again. |
tree | commitdiff |
| 2008-03-13 |
Claudio Sacerdoti... | :-( |
tree | commitdiff |
| 2008-03-13 |
Claudio Sacerdoti... | New version of freescale: |
tree | commitdiff |
| 2008-03-12 |
Claudio Sacerdoti... | Problem solved (was: apply needed an argument to avoid... |
tree | commitdiff |
| 2008-03-12 |
Claudio Sacerdoti... | Almost always correct optimization: during unification... |
tree | commitdiff |
| 2008-03-12 |
Enrico Tassi | fixed implicit |
tree | commitdiff |
| 2008-03-12 |
Andrea Asperti | Nuova dimostrazione riflessiva di le_to_Bertrand. |
tree | commitdiff |
| 2008-03-12 |
Enrico Tassi | if -debug is specified do not catch all exceptions |
tree | commitdiff |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
tree | commitdiff |
| 2008-03-10 |
Enrico Tassi | fixed wrong dependencies in debian package reported... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Bad hack to avoid failure of conversion (unfolding... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Scripts fixed because of: |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | whd: ~delta=false now controls also zeta-reduction... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | An unimplemented case of clearbody is now implemented. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | check_metasenv_consistency: |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Example query fixed. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Debugging print removed. |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Added ad-hoc optimization for check_metasenv_consistenc... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Performance improvement: let-ins should always be pushe... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Scripts fixed. They were broken since the change to... |
tree | commitdiff |
| 2008-03-09 |
Ferruccio Guidi | LAMBDA-TYPES: some more generation lemmas and some... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Potentially (and, at least sometimes, actually) big... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Redundant check (because of an invariant) removed. |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | * please let the library in shape * |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | fixed |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | skipped freescale and dama_didactic |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | fixed deps |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | reworked freescale stuff to put \m as a left parameter |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | no more assembly/ to skip |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | fix typo |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | added mkdir |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-03-05 |
Ferruccio Guidi | some corrections and additions |
tree | commitdiff |
| 2008-03-05 |
Enrico Tassi | from now on, export MATITA_EXTRACT=true to extract |
tree | commitdiff |
| 2008-03-05 |
Enrico Tassi | verbosity increased in case of error |
tree | commitdiff |
| 2008-03-04 |
Ferruccio Guidi | components/library: dotdothack removed |
tree | commitdiff |
| 2008-03-04 |
Claudio Sacerdoti... | New syntax for patterns. |
tree | commitdiff |
| 2008-03-04 |
Claudio Sacerdoti... | prodT ==> prod |
tree | commitdiff |
| 2008-03-04 |
Claudio Sacerdoti... | A) New version. |
tree | commitdiff |
| 2008-02-29 |
Ferruccio Guidi | we added the classic substitution function |
tree | commitdiff |
| 2008-02-28 |
Enrico Tassi | firs attempt to compile with ocamlbuild |
tree | commitdiff |
| 2008-02-27 |
Wilmer Ricciotti | the proof of bertrand's conjecture is now complete |
tree | commitdiff |
| 2008-02-26 |
Ferruccio Guidi | I added some debugging information |
tree | commitdiff |
| 2008-02-26 |
Ferruccio Guidi | added MATITAOPTIONS -onepass as for LAMBDA-TYPES |
tree | commitdiff |
| 2008-02-26 |
Ferruccio Guidi | LAMBDA-TYPES: added wf3 (legal context predicate); |
tree | commitdiff |
| 2008-02-24 |
Ferruccio Guidi | $(H) added :) |
tree | commitdiff |
| 2008-02-24 |
Ferruccio Guidi | LAMBDA-TYPES: dependences calculation improved |
tree | commitdiff |
| 2008-02-23 |
Ferruccio Guidi | LAMBDA-TYPES: |
tree | commitdiff |
| 2008-02-22 |
Ferruccio Guidi | - added some options to matitadep: -stdout and -exclude |
tree | commitdiff |
| 2008-02-22 |
Wilmer Ricciotti | sieve of erathostene (proof of soundness almost done) |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | A new very simple example for recursive functions.... |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Avoid translating back recursive fixes to the same... |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Avoid application to 0 arguments. |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Better handling of exceptions. |
tree | commitdiff |
| 2008-02-21 |
Ferruccio Guidi | svn:ignores fixed |
tree | commitdiff |
| 2008-02-20 |
Ferruccio Guidi | -onepass option removed from Makefile to comile Base... |
tree | commitdiff |
| 2008-02-20 |
Ferruccio Guidi | LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | splat_args is now better understood and debugged: we... |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | added small test, fixed some bugs |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | many fixed in translation functions |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | dependences needed a fix :) |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | we are moving the devel root one dir level up |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | snapshot inverse tranformation |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | transformation almost finisced, not tested |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | now inline "file.ma" is allowed. |
tree | commitdiff |
| 2008-02-19 |
Andrea Asperti | Added o.ma (some results about the magnitude of functio... |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | initial steps of convertibility |
tree | commitdiff |
| 2008-02-18 |
Enrico Tassi | some bits of reduction, reusing psubst |
tree | commitdiff |
| 2008-02-18 |
Andrea Asperti | Complete proof of Bertrand for n >= 256. |
tree | commitdiff |
| 2008-02-14 |
Andrea Asperti | Prima versione di bertrand. Tanti cambiamenti qua e la. |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | baseuris removed from files |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | fixed dependences |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | conversion half inplemented |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | reordered cases |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | reorganization of sources |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | substituion and lifting implemented |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | factorized common components of objects |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | added Local pragma, moved leftno and inductive into... |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | added leftno to indtypes, better indentation and comments |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | nCic almost finished |
tree | commitdiff |
| 2008-02-12 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-12 |
Ferruccio Guidi | regeneration with new results |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | fixed path for matitadep |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | fixed make dist |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | better error message in case inclusion failed |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | allow to use "../foo/bar.ma" as a path for the include... |
tree | commitdiff |
| 2008-02-08 |
Andrea Asperti | progress. |
tree | commitdiff |
| 2008-02-08 |
Claudio Sacerdoti... | A formalization of modified realisability with truth... |
tree | commitdiff |
| next |
projects / helm.git / history