2005-09-27 |
Stefano Zacchiroli | added/exported pp_pos & pp_attribute |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | removed .annot files (files containing type annotations... |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Andrea Asperti | small error in nth_prime. |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Andrea Asperti | New entry: fermat's little theorem (almost complete). |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | more fine grained debug printing |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | changed type of ids_to_uris table to (Cic.id, UriManage... |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | Better handling of idref propagation, no more Href... |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | moved list_uniq to the extlib |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | added support for multiple idrefs |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | added list_uniq |
commit | commitdiff | tree | snapshot |
2005-09-27 |
Stefano Zacchiroli | completed use of \mod and / notation |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | coq.moo is now automatically generated. New targets: |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Enrico Tassi | fix WE HAVE NO UNIVERSE |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | fixed typo |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Enrico Tassi | ./matitaclean all removes all |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | strip heading '\' on Mo s |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | removed some dead code |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | if a node has an xref use it for cut and paste, no... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | coq.moo is now automatically generated |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | function composition notation |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | Coq's existential fixed. |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | div and mod notation ('%' and '\mod') |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | added override for \circ (notation for function composi... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | matitatop.opt should not be generated |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | Unification enhanchement. |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | Unification enhanchement: |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Claudio Sacerdoti... | Inclusion path fixed. |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Alberto Griggio | new paramodulation |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Alberto Griggio | *** empty log message *** |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Alberto Griggio | added apply_tac_verbose_with_subst, returning a Cic... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | added binary version of coq.moo and the corresponding... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | removed textual version of coq's moo file |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Enrico Tassi | MatitacleanLib.remove_baseuris will remove empty direct... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Andrea Asperti | permutation.ma added to the repository. |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Andrea Asperti | Small bug due to case unsensitiveness in the check... |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | changed default divide notation to a/b |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | bugfix: reash uris embedded in cic appl patterns |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | - added integrity checks on .moo files |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | better name for a theorem |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | added magic numbers |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | set extlib findlib dependencies |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Stefano Zacchiroli | implemented the first bunch of useful functions |
commit | commitdiff | tree | snapshot |
2005-09-26 |
Andrea Asperti | Mysql ==> HMysql |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | New module HMysql (to abstract over Mysql and make... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | New module HMysql (to abstract over Mysql and make... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | changed .moo format on disk: no longer plain strings... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | More profiling code. |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | CicUtil.profile ==> HExtlib.profile |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | CicUtil.profile ==> HExtlib.profile |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | bugfix: evaluation of object commands is now atomic... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | "verbose" argument of remove is now optional (default... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Less feedback during removal of objects. |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Too many OPTIMIZE TABLES (because of a very stupid... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | save_object_to_disk profiler fixed |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Profiling code removed. |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | several "INSERT VALUE" ==> "INSERT VALUES" (more efficient) |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Profiling code removed. |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | avoid generating useless parens in mathml contextes... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | removed a line of dead code |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Dead code removed again!!! |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | avoid pattern matching on attributed terms since this... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | fix |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | universes are saved to disk |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | The disambiguation now returns the aliases diff. It... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | added universes list handling |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | added universes |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | added parsing of Type:N |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | a wrong exception was raised |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Stefano Zacchiroli | bugfix for uminus notation, prints parens where needed |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Enrico Tassi | added support for universes uri ".univ" |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | The disambiguation now returns the aliases diff. It... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Andrea Asperti | log.ma renamed into ord.ma |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | The new_aliases argument of the functions alias_diff... |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Andrea Asperti | A few changes to factorization and gcd. |
commit | commitdiff | tree | snapshot |
2005-09-23 |
Claudio Sacerdoti... | Environment replaced by lists of domain and codomain... |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | More notation here and there: \sup, \divides, \ndivides, ! |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | * Added divides and ndivides |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | '!' is no longer a decorator (to allow a reasonable... |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | Profiling messages grepped out. |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2005-09-22 |
Claudio Sacerdoti... | Dead code removed |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | More profiling code. |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | This commit removes the slowest identity function ever... |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | We do not longer generate inner-types and inner-sorts... |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | We do not longer generate inner-types and inner-sorts... |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Stefano Zacchiroli | ported to the new parser interface (Ulexing.lexbuf... |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Stefano Zacchiroli | uses ligatures (as a sample) |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Stefano Zacchiroli | added ligatures support |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Stefano Zacchiroli | rebuilt |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Enrico Tassi | clean_and_fill optimization |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Alberto Griggio | bugfix on proof construction |
commit | commitdiff | tree | snapshot |
2005-09-21 |
Claudio Sacerdoti... | All the debug_print are now lazy. |
commit | commitdiff | tree | snapshot |
next |