| 2007-07-24 |
Ferruccio Guidi | New developement LOGIC about the cut elimination of... |
commit | commitdiff | tree | snapshot |
| 2007-07-24 |
Enrico Tassi | added test about dependent coercions |
commit | commitdiff | tree | snapshot |
| 2007-07-23 |
Claudio Sacerdoti... | Prototype of min_aux changed. |
commit | commitdiff | tree | snapshot |
| 2007-07-23 |
Ferruccio Guidi | auto vs autobatch fixed |
commit | commitdiff | tree | snapshot |
| 2007-07-23 |
Ferruccio Guidi | autobatch parameters reajusted |
commit | commitdiff | tree | snapshot |
| 2007-07-23 |
Enrico Tassi | fixed makefiles to make it compile cleanly again |
commit | commitdiff | tree | snapshot |
| 2007-07-22 |
Ferruccio Guidi | Procedural: the statement body and it inner types must... |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | Another nicer version. |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | Even nicer script. |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | The nicest script obtained so far. |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Ferruccio Guidi | acic_procedural: bug fix: |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | More simplification due to the new conversion strategy. |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | Script simplification due to the new efficient conversi... |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | Tentative bug fix for diverging pretty-printing function. |
commit | commitdiff | tree | snapshot |
| 2007-07-20 |
Claudio Sacerdoti... | Initialization of matita.map_unicode_to_tex moved from... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Ferruccio Guidi | cicUtil : new test function "is_sober" to test... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Claudio Sacerdoti... | Convertibility now converts machines in place of terms. |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Claudio Sacerdoti... | map_unicode_to_tex is no longer optional and it always... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Claudio Sacerdoti... | paste_unicode_as_tex is now false by default; moreover... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Enrico Tassi | COERCIONS: tentative addition of an equivalence relatio... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Enrico Tassi | the cade was escaping the table name and not the uri |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Enrico Tassi | fixed escaping for sqlite |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Enrico Tassi | fixed an escaping error, added more infos to the generi... |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Claudio Sacerdoti... | Typo fixed. |
commit | commitdiff | tree | snapshot |
| 2007-07-19 |
Claudio Sacerdoti... | Super-nice notation for the assembly stuff. |
commit | commitdiff | tree | snapshot |
| 2007-07-18 |
Ferruccio Guidi | the predicate for elim was not built correctly when... |
commit | commitdiff | tree | snapshot |
| 2007-07-18 |
Enrico Tassi | recursive argument in let rec is not printed explicitly. |
commit | commitdiff | tree | snapshot |
| 2007-07-18 |
Enrico Tassi | fixed coercion graph print, moved coercion graph and... |
commit | commitdiff | tree | snapshot |
| 2007-07-17 |
Claudio Sacerdoti... | added missing parenthesis |
commit | commitdiff | tree | snapshot |
| 2007-07-17 |
Enrico Tassi | fixed includes and added notation for bytes |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | More lemmas. |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons closed. A couple left in byte and many... |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons/axioms closed. |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | One daemon less. |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons got rid of (and more extra axioms to be... |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | Last daemon killed :-) |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | One less daemon (about "update"s). |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | All sub-proofs about "update" closed. |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Claudio Sacerdoti... | assembly.ma splitted into many files |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * NOT RELEASED YET |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * NOT RELEASED YET |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | proper path for ps.gz doc |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | texlive-base-bin, texlive-latex-extra |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | - add build-dep for doc generation: graphviz, texlive... |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | - add build-dep for doc generation: graphviz, texlive... |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * debian/rules |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | invoke make doc after build to create ocamldoc docs |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * debian/svn-deblayout |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * rebuild against OCaml 3.10 and ocamlnet 2.2 |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * debian/*.install.in |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Stefano Zacchiroli | * rebuild with OCaml 3.10 |
commit | commitdiff | tree | snapshot |
| 2007-07-16 |
Wilmer Ricciotti | corrected axiom mod_plus |
commit | commitdiff | tree | snapshot |
| 2007-07-14 |
Ferruccio Guidi | new definitions and new theorems |
commit | commitdiff | tree | snapshot |
| 2007-07-13 |
Claudio Sacerdoti... | More conjectures closed. |
commit | commitdiff | tree | snapshot |
| 2007-07-13 |
Claudio Sacerdoti... | 1. requires the new pretty printer for natural numbers |
commit | commitdiff | tree | snapshot |
| 2007-07-13 |
Claudio Sacerdoti... | Dirty patch by Zack: natural numbers of Matita are... |
commit | commitdiff | tree | snapshot |
| 2007-07-13 |
Claudio Sacerdoti... | Last crazy commit reverted. |
commit | commitdiff | tree | snapshot |
| 2007-07-13 |
Claudio Sacerdoti... | Final theorem proved. Many many conjectures left. I... |
commit | commitdiff | tree | snapshot |
| 2007-07-12 |
Claudio Sacerdoti... | The loop invariant I chosed was not correct! |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Claudio Sacerdoti... | Getting close to the final result. |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Claudio Sacerdoti... | 1. loop invariant stated, but not proved |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Ferruccio Guidi | native dependences fixed |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Claudio Sacerdoti... | 1. status factorized out in tick |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Claudio Sacerdoti... | auto new => autobatch |
commit | commitdiff | tree | snapshot |
| 2007-07-11 |
Claudio Sacerdoti... | auto new => autobatch |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Claudio Sacerdoti... | 0. less nice solution by Enrico reverted |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Claudio Sacerdoti... | New reduction strategy: the new reduction strategy... |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Enrico Tassi | La programmazione funzionale e' come TeX, funziona... |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Ferruccio Guidi | persistent inner types are now generated in publishing... |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Enrico Tassi | fixed a bug in the cleanup ofsedir that was not properl... |
commit | commitdiff | tree | snapshot |
| 2007-07-10 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Enrico Tassi | 1. bug fixed in tick |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Enrico Tassi | signal hadler restored after runnig external 'make' |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Claudio Sacerdoti... | Interesting theorem added (but still to be proved). |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Enrico Tassi | added few more fun to this test |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Ferruccio Guidi | new configuration file sample |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Ferruccio Guidi | tassi: ported to the new DB architecture. |
commit | commitdiff | tree | snapshot |
| 2007-07-09 |
Enrico Tassi | auto->autobatch |
commit | commitdiff | tree | snapshot |
| 2007-07-07 |
Enrico Tassi | inclusion of div_and_mod |
commit | commitdiff | tree | snapshot |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
commit | commitdiff | tree | snapshot |
| 2007-07-05 |
Claudio Sacerdoti... | Exadecimal numbers are now used. This is a great speed-up. |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | Example program executed for x,y=0. |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | Quick hack: matita natural numbers are now accepted... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | Bug fixed: a ~with_cast is now inserted when appropriat... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | In place of conclude, obtain FIXMEXXX is now generated... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | 1. Code simplification |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | is_top_down was not propageted correctly under a bottom... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | 1. "by proof" now allowed as a justification in equalit... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | Added ~with_cast to the change tactic. |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | Bug fixed: name in letin was printed as "previous"... |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | More opcodes (badly) implemented. |
commit | commitdiff | tree | snapshot |
| 2007-07-04 |
Claudio Sacerdoti... | List.ma: added function nth (with default value in... |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Cristian Armentano | New definition of Euler's totient function. |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Claudio Sacerdoti... | In order to generate executable declarative scripts... |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Claudio Sacerdoti... | Bug fixed in bottom-up conversion. |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Claudio Sacerdoti... | BU Conversion was not generated for Rels fixed. I wonde... |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Claudio Sacerdoti... | Nicer layout but possibly more bugged. |
commit | commitdiff | tree | snapshot |
| 2007-06-30 |
Claudio Sacerdoti... | Spurious "we need to prove" at the beginning of Intros... |
commit | commitdiff | tree | snapshot |
| 2007-06-29 |
Cristian Armentano | generic version, specializing generic_sigma_p.ma |
commit | commitdiff | tree | snapshot |
| 2007-06-29 |
Cristian Armentano | generic version |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog