| 2007-10-14 | Claudio Sacerdoti... | Some lemmas moves to the file they belong to. | commit | commitdiff | tree | snapshot | 
| 2007-10-14 | Cristian Armentano | Theorem sigma_p_knm changed into generic_iter_p_knm. | commit | commitdiff | tree | snapshot | 
| 2007-10-13 | Ferruccio Guidi | - some new auxiliary lemmas | commit | commitdiff | tree | snapshot | 
| 2007-10-13 | Ferruccio Guidi | removed unused notation => | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Wilmer Ricciotti | Fixed baseuri | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Wilmer Ricciotti | Part1a update... | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Andrea Asperti | More restructuring in moebius.ma | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Andrea Asperti | Reorganization of the library. | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Andrea Asperti | Reorganization of the library. | commit | commitdiff | tree | snapshot | 
| 2007-10-12 | Andrea Asperti | Reorganization of results. | commit | commitdiff | tree | snapshot | 
| 2007-10-11 | Claudio Sacerdoti... | Old inversion bug fixed: it used to work only on the... | commit | commitdiff | tree | snapshot | 
| 2007-10-09 | Enrico Tassi | added patch to allow i,j,k: skip and *: skip | commit | commitdiff | tree | snapshot | 
| 2007-10-08 | Andrea Asperti | Some axioms for Q. | commit | commitdiff | tree | snapshot | 
| 2007-09-27 | Ferruccio Guidi | added some notation | commit | commitdiff | tree | snapshot | 
| 2007-09-26 | Ferruccio Guidi | started the Proof Weight predicate for cut elimination... | commit | commitdiff | tree | snapshot | 
| 2007-09-25 | Ferruccio Guidi | bug fix in Track definition | commit | commitdiff | tree | snapshot | 
| 2007-09-24 | Wilmer Ricciotti | Last version of poplmark 1a, featuring new proof, only... | commit | commitdiff | tree | snapshot | 
| 2007-09-23 | Ferruccio Guidi | we chmod the created directories to override the umask... | commit | commitdiff | tree | snapshot | 
| 2007-09-23 | Ferruccio Guidi | fixed some file permissions (anybody can rebuild a... | commit | commitdiff | tree | snapshot | 
| 2007-09-22 | Ferruccio Guidi | - system flag now forks for matitadep too | commit | commitdiff | tree | snapshot | 
| 2007-09-22 | Stefano Zacchiroli | * add Homepage debian/control field | commit | commitdiff | tree | snapshot | 
| 2007-09-21 | Ferruccio Guidi | bug fix in configuration dependences | commit | commitdiff | tree | snapshot | 
| 2007-09-21 | Ferruccio Guidi | now the -bench and -system flags work for matitamake | commit | commitdiff | tree | snapshot | 
| 2007-09-20 | Cristian Armentano | Further simplifications to the main theorem about Euler... | commit | commitdiff | tree | snapshot | 
| 2007-09-19 | Cristian Armentano | * Some simplifications to theorem in file totient1.ma. | commit | commitdiff | tree | snapshot | 
| 2007-09-19 | Enrico Tassi | commented out pack coercion, since the code is not... | commit | commitdiff | tree | snapshot | 
| 2007-09-18 | Cristian Armentano | some theorems have been moved to more appropriate files... | commit | commitdiff | tree | snapshot | 
| 2007-09-17 | Cristian Armentano | temporary changes, before the complete cancellation... | commit | commitdiff | tree | snapshot | 
| 2007-09-17 | Cristian Armentano | simplified version of a theorem. | commit | commitdiff | tree | snapshot | 
| 2007-09-17 | Andrea Asperti | Some new lemmas. | commit | commitdiff | tree | snapshot | 
| 2007-09-17 | Andrea Asperti | A new function. | commit | commitdiff | tree | snapshot | 
| 2007-09-15 | Stefano Zacchiroli | unreleased | commit | commitdiff | tree | snapshot | 
| 2007-09-15 | Stefano Zacchiroli | * debian/liblablgtkmathview-ocaml-dev.install.in | commit | commitdiff | tree | snapshot | 
| 2007-09-15 | Ferruccio Guidi | utf8 changed to UTF-8 for compatibility with IExplorer | commit | commitdiff | tree | snapshot | 
| 2007-09-14 | Andrea Asperti | Qualche semplificazione. | commit | commitdiff | tree | snapshot | 
| 2007-09-14 | Enrico Tassi | since compat <> 3 no cmx* in the install.in bu just cm* | commit | commitdiff | tree | snapshot | 
| 2007-09-14 | Ferruccio Guidi | this preamble was completely wrong :) | commit | commitdiff | tree | snapshot | 
| 2007-09-13 | Ferruccio Guidi | a working example :) | commit | commitdiff | tree | snapshot | 
| 2007-09-13 | Ferruccio Guidi | the published devels must be removed from the tests | commit | commitdiff | tree | snapshot | 
| 2007-09-13 | Ferruccio Guidi | new matita.conf with getter entry to see the published... | commit | commitdiff | tree | snapshot | 
| 2007-09-13 | Claudio Sacerdoti... | added a debug print | commit | commitdiff | tree | snapshot | 
| 2007-09-12 | Ferruccio Guidi | rdfly patched to work with the new db structure | commit | commitdiff | tree | snapshot | 
| 2007-09-12 | Wilmer Ricciotti | Updated, proofs are now about 750 lines. | commit | commitdiff | tree | snapshot | 
| 2007-09-11 | Ferruccio Guidi | librarySync - we do not generate the object attributes... | commit | commitdiff | tree | snapshot | 
| 2007-09-11 | Cristian Armentano | some theorem names changed. | commit | commitdiff | tree | snapshot | 
| 2007-09-11 | Enrico Tassi | replaced an assert false that cause nat_ind not to... | commit | commitdiff | tree | snapshot | 
| 2007-09-10 | Enrico Tassi | last version with caml 3.09 built and saved as 0.3.0 | commit | commitdiff | tree | snapshot | 
| 2007-09-10 | Enrico Tassi | ... | commit | commitdiff | tree | snapshot | 
| 2007-09-10 | Cristian Armentano | other simplifications. | commit | commitdiff | tree | snapshot | 
| 2007-09-10 | Claudio Sacerdoti... | This test shows one of the few cases were Matita is... | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Stefano Zacchiroli | * debian/control | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Enrico Tassi | ... | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Enrico Tassi | in the case of coerce_to_sort the whd was done with... | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Cristian Armentano | other simplifications. | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Stefano Zacchiroli | * NOT RELEASED YET | commit | commitdiff | tree | snapshot | 
| 2007-09-09 | Stefano Zacchiroli | * change how the ocamldoc API reference is generated... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | huge commit regarding coercions to funclass and eat_pro... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | the order of abstraction is now correct, but there... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | removed an assertion that makes no more sense to me | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | better debug printings | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | better test for church numerals | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | just a Pcre expression fixed, nothing real | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | ... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | matita can now safely start a matitac that will put... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Enrico Tassi | Full specification of find. Added notation for If_Then_... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | bump version | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | release | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | * add ocamldoc comments to .mli interface files | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | include also gdome2/ dir in the ocamldoc include path | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | * debian/rules | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | why the heck configure was committed? | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | * debian/control | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | init new dummy entry | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | remove spurious comment | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | upload to unstable | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | remove spurious entry | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | - s/Source-Version/binary:Version/ substvar | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | add stdlib/gdome2 to the include dir for ocamldoc | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | bump version | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | * convert comments in .mli interface files to ocamldoc... | commit | commitdiff | tree | snapshot | 
| 2007-09-08 | Stefano Zacchiroli | convert comments to ocamldoc comments | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | 1. fix_arity fixed: the code is totally wrong and this... | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | This cast now works! | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | when a coercion is passed through a case on right-param... | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Cristian Armentano | some simplifications. | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | ooops, missing ) | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | disabled coercions when refining paramod proofs (attemt... | commit | commitdiff | tree | snapshot | 
| 2007-09-07 | Enrico Tassi | fixed propagation under Fix/Lambda/Case of coercions... | commit | commitdiff | tree | snapshot | 
| 2007-09-06 | Cristian Armentano | Some simplifications. | commit | commitdiff | tree | snapshot | 
| 2007-09-06 | Enrico Tassi | coercions under Fix and Case. Code refactoring needed | commit | commitdiff | tree | snapshot | 
| 2007-09-06 | Enrico Tassi | added a duplicated implementation of replace lifting | commit | commitdiff | tree | snapshot | 
| 2007-09-06 | Enrico Tassi | ... | commit | commitdiff | tree | snapshot | 
| 2007-09-05 | Ferruccio Guidi | - lybrarySync: | commit | commitdiff | tree | snapshot | 
| 2007-09-05 | Ferruccio Guidi | - matitaInit matitaprover matitadep matitamake: | commit | commitdiff | tree | snapshot | 
| 2007-09-05 | Claudio Sacerdoti... | added fix case | commit | commitdiff | tree | snapshot | 
| 2007-09-05 | Claudio Sacerdoti... | coercions are propagated under Fix (but not mutually... | commit | commitdiff | tree | snapshot | 
| 2007-09-04 | Claudio Sacerdoti... | Dandling ")" removed from notation for 'exists. | commit | commitdiff | tree | snapshot | 
| 2007-09-04 | Claudio Sacerdoti... | Composition of coercions with arity > 0 is now implemen... | commit | commitdiff | tree | snapshot | 
| 2007-09-04 | Claudio Sacerdoti... | A test for propagation of coercions (that open new... | commit | commitdiff | tree | snapshot | 
| next |