| 2005-09-26 |
no author | This commit was manufactured by cvs2svn to create tag LAST_BEFORE_NEW |
tree | commitdiff |
| 2005-09-26 |
Alberto Griggio | *** empty log message *** |
tree | commitdiff |
| 2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument... |
tree | commitdiff |
| 2005-09-26 |
Alberto Griggio | added apply_tac_verbose_with_subst, returning a Cic... |
tree | commitdiff |
| 2005-09-26 |
Andrea Asperti | Small bug due to case unsensitiveness in the check... |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | bugfix: reash uris embedded in cic appl patterns |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | added magic numbers |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | set extlib findlib dependencies |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | implemented the first bunch of useful functions |
tree | commitdiff |
| 2005-09-26 |
Andrea Asperti | Mysql ==> HMysql |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | New module HMysql (to abstract over Mysql and make... |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | More profiling code. |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | CicUtil.profile ==> HExtlib.profile |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-23 |
Claudio Sacerdoti... | Profiling code removed. |
tree | commitdiff |
| 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 | 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 |
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 |
Claudio Sacerdoti... | Environment replaced by lists of domain and codomain... |
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... | 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 |
Stefano Zacchiroli | ported to the new parser interface (Ulexing.lexbuf... |
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 |
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 | added a minimal parser to extract informations relevant... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Profiling disabled. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | This commit (partially) removes a big source of ineffic... |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | - bugfix: when backtracking restore the appropriate... |
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 |
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 |
Stefano Zacchiroli | bugfix in discriminate: now works also with inductive... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | uniformed ppmetasenv to other pp* methods: substs are... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | bugfix: default "false" used to set the _true_ uri ... |
tree | commitdiff |
| 2005-09-14 |
Stefano Zacchiroli | done some items |
tree | commitdiff |
| 2005-09-14 |
Stefano Zacchiroli | added hyperlinks on case pattern heads and outtype |
tree | commitdiff |
| 2005-09-13 |
Claudio Sacerdoti... | Enabling/disabling profiling is now controlled by a... |
tree | commitdiff |
| 2005-09-13 |
Enrico Tassi | we have to pass back lastmeta and not newmeta (newmeta... |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | fixed "let .. in" rendering, adding the break between... |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | added "commands_of_environment" |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | regenerated |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | moved dummy_floc from Disambiguate to DisambiguateTypes... |
tree | commitdiff |
| 2005-09-13 |
Claudio Sacerdoti... | Two bugs fixed in the apply tactic: |
tree | commitdiff |
| 2005-09-12 |
Claudio Sacerdoti... | cic_textual_parser2 ==> cic_disambiguation |
tree | commitdiff |
| 2005-09-12 |
Claudio Sacerdoti... | cic_textual_parser2 ==> cic_disambiguation |
tree | commitdiff |
| 2005-09-12 |
Claudio Sacerdoti... | core_notation.ma ==> core_notation.moo |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | cic_textual_parser2 -> cic_disambiguation |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | removed debugging print |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | added support for multi-aliases in disambiguation envir... |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | added use_coercions flag (imperative :-(, non re-entran... |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | - exported CPS iterator visit_magic |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | Filled pre-generated notation levels with productions... |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | done some items |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | commented Record type constructor |
tree | commitdiff |
| 2005-09-09 |
Enrico Tassi | the case Appl Meta vs t was not executed in case t... |
tree | commitdiff |
| 2005-09-08 |
Stefano Zacchiroli | removed some debugging prints |
tree | commitdiff |
| 2005-09-08 |
Stefano Zacchiroli | implemented lazy disambiguation of tactics arguments... |
tree | commitdiff |
| 2005-09-08 |
Stefano Zacchiroli | uses Map.equal to compare universes |
tree | commitdiff |
| 2005-09-07 |
Claudio Sacerdoti... | Unsharing bugs fixed. |
tree | commitdiff |
| 2005-09-07 |
Claudio Sacerdoti... | Unsharing bug due to a very stupid typo fixed. |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | bugfix: avoid losing attributes on boxes which have... |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | removed dead code |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | added {get,set}_attr |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | added {get,set,pp}_attr |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | uses \def symbol for definitions in context |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | updated |
tree | commitdiff |
| 2005-09-06 |
Alberto Griggio | added dirty hack to blacklist mult_n_2, which causes... |
tree | commitdiff |
| 2005-09-06 |
Claudio Sacerdoti... | Refiner substituted with the type-checker in a case... |
tree | commitdiff |
| 2005-09-06 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2005-09-06 |
Claudio Sacerdoti... | Dead code/files removed. |
tree | commitdiff |
| 2005-09-06 |
Stefano Zacchiroli | removed debugging prints and better sample |
tree | commitdiff |
| next |
projects / helm.git / history