| 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 |
| 2005-09-06 |
Stefano Zacchiroli | added <include href="foo/bar/baz.xml" /> support |
tree | commitdiff |
| 2005-09-06 |
Claudio Sacerdoti... | Serious bug fixed: unsharing was not performed over... |
tree | commitdiff |
| 2005-09-06 |
Claudio Sacerdoti... | Dead code removed. |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | Unfold tactic generalized to perform zeta-reduction. |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | locate_in_* functions generalized to handle equalities... |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | New change in patterns: the pattern "in H" is now inter... |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | The refined form of a reference to a let-in bound varia... |
tree | commitdiff |
| 2005-09-05 |
Stefano Zacchiroli | use uniform naming for referencing cicNotation* modules |
tree | commitdiff |
| 2005-09-05 |
Stefano Zacchiroli | removed tedious debugging message |
tree | commitdiff |
| 2005-09-05 |
Stefano Zacchiroli | avoid generating multiple times the same xref/href |
tree | commitdiff |
| 2005-09-05 |
Enrico Tassi | fix generation of applications of applications. |
tree | commitdiff |
| 2005-09-05 |
Enrico Tassi | added @raise in comment (and source) |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | New strategy for let-in unfolding (aka zeta reduction... |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | Critical bug fixed: the get_cooked_obj was called on... |
tree | commitdiff |
| 2005-09-05 |
Claudio Sacerdoti... | Bug fixed: Invalid_argument was raised by List.combine... |
tree | commitdiff |
| 2005-09-02 |
Claudio Sacerdoti... | Unsharing finally introduced (but just for object proce... |
tree | commitdiff |
| 2005-09-02 |
Claudio Sacerdoti... | Bug fixed: sorts and implicits were not unshared correctly. |
tree | commitdiff |
| 2005-09-02 |
Claudio Sacerdoti... | Assert added to check whether an unsharing problem... |
tree | commitdiff |
| 2005-09-02 |
Claudio Sacerdoti... | Serious bug fixed previously introduced by me in the... |
tree | commitdiff |
| 2005-09-02 |
Claudio Sacerdoti... | Unused index (because of UNIQUE field count) dropped. |
tree | commitdiff |
| 2005-09-01 |
Claudio Sacerdoti... | New index refObj_occurrence on refObj. It is required... |
tree | commitdiff |
| 2005-09-01 |
Alberto Griggio | changed default parameter values... |
tree | commitdiff |
| 2005-09-01 |
Claudio Sacerdoti... | Comment added. |
tree | commitdiff |
| 2005-08-31 |
Alberto Griggio | fixed bug in compute_equality_weight caused by wrong... |
tree | commitdiff |
| 2005-08-30 |
Claudio Sacerdoti... | Bug fixed: "cic:/dummy_i" is an invalid URI (that used... |
tree | commitdiff |
| 2005-08-30 |
Claudio Sacerdoti... | A parser for aliases implemented (required by the Whelp). |
tree | commitdiff |
| 2005-08-30 |
Claudio Sacerdoti... | CicNotationPres self-reference (misteriously accepted... |
tree | commitdiff |
| 2005-08-29 |
Claudio Sacerdoti... | WARNING: this commit changes the DB representation... |
tree | commitdiff |
| 2005-08-22 |
Alberto Griggio | some fixes |
tree | commitdiff |
| 2005-08-12 |
Stefano Zacchiroli | improved some comments |
tree | commitdiff |
| 2005-08-05 |
Alberto Griggio | some bugs fixed |
tree | commitdiff |
| 2005-08-01 |
Alberto Griggio | fixed compilation warnings |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | 1. ProofEngineHelpers.locate_in_term, ProofEngineHelper... |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | Bug fixed: unfold used to work iff the term to unfold... |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | arguments of ProofEngineHelpers.replace swapped. |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | Bug fixed: locate_term_in_conjecture used to raise... |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | New tactic unfold. |
tree | commitdiff |
| 2005-07-28 |
Stefano Zacchiroli | added pretty printing of unicode symbols to TeX like... |
tree | commitdiff |
| 2005-07-28 |
Stefano Zacchiroli | added attributes re-factoring item |
tree | commitdiff |
| 2005-07-28 |
Stefano Zacchiroli | added reverse mapping from unicode to TeX like macro... |
tree | commitdiff |
| 2005-07-28 |
Stefano Zacchiroli | workaround for an assertion failure during rendering... |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | fixed cic_notation dependencies |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | better boxes (with more line breaking hints) for object... |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | *** empty log message *** |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | bugfix: added xref on ast built via pattern matching... |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | added id_of_annterm: Cic.annterm -> Cic.id |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | bugfix: no more xref on bound names |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | added low level rendering attributes (indent, spacing... |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | rendering from markup to string |
tree | commitdiff |
| 2005-07-27 |
Stefano Zacchiroli | improved debugging pretty printing of xref |
tree | commitdiff |
| 2005-07-26 |
Claudio Sacerdoti... | locate_in_term generalized to locate_in_conjecture |
tree | commitdiff |
| next |
projects / helm.git / history