| 2005-09-23 |
Claudio Sacerdoti... | several "INSERT VALUE" ==> "INSERT VALUES" (more efficient) |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | Profiling code removed. |
tree | commitdiff |
| 2005-09-23 |
Stefano Zacchiroli | avoid generating useless parens in mathml contextes... |
tree | commitdiff |
| 2005-09-23 |
Stefano Zacchiroli | removed a line of dead code |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | Dead code removed again!!! |
tree | commitdiff |
| 2005-09-23 |
Stefano Zacchiroli | avoid pattern matching on attributed terms since this... |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | fix |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | universes are saved to disk |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | The disambiguation now returns the aliases diff. It... |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | added universes list handling |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | added universes |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | added parsing of Type:N |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | a wrong exception was raised |
tree | commitdiff |
| 2005-09-23 |
Stefano Zacchiroli | bugfix for uminus notation, prints parens where needed |
tree | commitdiff |
| 2005-09-23 |
Enrico Tassi | added support for universes uri ".univ" |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | The disambiguation now returns the aliases diff. It... |
tree | commitdiff |
| 2005-09-23 |
Andrea Asperti | log.ma renamed into ord.ma |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | The new_aliases argument of the functions alias_diff... |
tree | commitdiff |
| 2005-09-23 |
Andrea Asperti | A few changes to factorization and gcd. |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | Environment replaced by lists of domain and codomain... |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there: \sup, \divides, \ndivides, ! |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | * Added divides and ndivides |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | '!' is no longer a decorator (to allow a reasonable... |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | Profiling messages grepped out. |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | Dead code removed |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | More profiling code. |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | This commit removes the slowest identity function ever... |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | We do not longer generate inner-types and inner-sorts... |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | We do not longer generate inner-types and inner-sorts... |
tree | commitdiff |
| 2005-09-21 |
Stefano Zacchiroli | ported to the new parser interface (Ulexing.lexbuf... |
tree | commitdiff |
| 2005-09-21 |
Stefano Zacchiroli | uses ligatures (as a sample) |
tree | commitdiff |
| 2005-09-21 |
Stefano Zacchiroli | added ligatures support |
tree | commitdiff |
| 2005-09-21 |
Stefano Zacchiroli | rebuilt |
tree | commitdiff |
| 2005-09-21 |
Enrico Tassi | clean_and_fill optimization |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-21 |
Alberto Griggio | bugfix on proof construction |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | All the debug_print are now lazy. |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | More debug_print made lazy. |
tree | commitdiff |
| 2005-09-21 |
Claudio Sacerdoti... | 1. profiling code added |
tree | commitdiff |
| 2005-09-20 |
Claudio Sacerdoti... | Profiling did not profile functions that raise an excep... |
tree | commitdiff |
| 2005-09-20 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-20 |
Claudio Sacerdoti... | More profiling code added. |
tree | commitdiff |
| 2005-09-20 |
Claudio Sacerdoti... | More profiling code inserted. |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | added non-builtin notation for exists |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | changed ast representation of exists |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | pretty printing of literals is now subject to the debug... |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | changed ast representation of exists, now an 'exists... |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | bugfix in default magic handling: consider as having... |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | - bugfix: eta abstractions ignores attributed node... |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | more refere to bindings in env type definition |
tree | commitdiff |
| 2005-09-20 |
Enrico Tassi | fixed matitadep: now it should consider ALL depndencies |
tree | commitdiff |
| 2005-09-20 |
Enrico Tassi | added a minimal parser to extract informations relevant... |
tree | commitdiff |
| 2005-09-20 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-20 |
Enrico Tassi | all initialization code is now in the new matitaInit... |
tree | commitdiff |
| 2005-09-20 |
Enrico Tassi | matitadep now parses notation. |
tree | commitdiff |
| 2005-09-20 |
Enrico Tassi | development windows now avoids doing an anction selecti... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | * Obsolete debugging comments removed |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Notation for "ex" introduced. It is the same as the... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | More profiling code. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Great speed-up in alias_diff (about 3x). |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | A bit of profiling functions added here and there. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Spurious interpretation removed. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Profiling disabled. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | This commit (partially) removes a big source of ineffic... |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | added list.ma |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | - avoid catching top level exceptions when the relevant... |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | splitted command line arguments among debugging and... |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | - added support for -debug, which avoid catching top... |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | - bugfix: when backtracking restore the appropriate... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Removed final question marks from {apply|elim|rewrite}s. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Some code that used to avoid a fixed bug removed. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | .ma inclusions corrected/minimized |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Profiling code commented out. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | CicUtil.profile made even more polymorphic. |
tree | commitdiff |
| 2005-09-16 |
Enrico Tassi | added a function to reorder the metasenv. |
tree | commitdiff |
| 2005-09-16 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-16 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | added notation for: nleq, ngeq, nless, and ngtr |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | added notation for nleq, nlgt, ... |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | added entites/overrides for leq, geq, nleq, ngeq, to |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | re-generated |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | uses Hashtbl.replace instead of Hashtbl.add so that: |
tree | commitdiff |
| 2005-09-15 |
Claudio Sacerdoti... | Yet another implementation of the single aliases /... |
tree | commitdiff |
| 2005-09-15 |
Claudio Sacerdoti... | "bool.ma" is now always included before "logic.ma"... |
tree | commitdiff |
| 2005-09-15 |
Claudio Sacerdoti... | Yet another implementation of the single aliases /... |
tree | commitdiff |
| 2005-09-15 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | improved discriminate test: check if it works on induct... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | bugfix in discriminate: now works also with inductive... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | added \neq notation |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | bugfix: save "~" backup together with the non-~ version... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | added -debug flag which avoid catching top-level except... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | - changed command line interface of cicbrowser so that... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | uniformed ppmetasenv to other pp* methods: substs are... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | moved matita logo in the right place |
tree | commitdiff |
| next |
projects / helm.git / history