| 2009-10-28 |
Enrico Tassi | do not put " around node name, otherwise names like... |
tree | commitdiff |
| 2009-10-28 |
Enrico Tassi | export group_by_tac |
tree | commitdiff |
| 2009-10-23 |
Enrico Tassi | added code to print the tree |
tree | commitdiff |
| 2009-10-23 |
Enrico Tassi | more functions |
tree | commitdiff |
| 2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope... |
tree | commitdiff |
| 2009-10-22 |
Enrico Tassi | the trie indexes terms up to 10 nested applications... |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | first bits for the zipper |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | more printings |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | nauto: |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | preserve sharing if map_term_fold_a |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | add XXX where I found a catch all statement |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | new sharing-preserving map with accumulator |
tree | commitdiff |
| 2009-10-21 |
Enrico Tassi | apply the subst to the metasenv and to p |
tree | commitdiff |
| 2009-10-20 |
Claudio Sacerdoti... | - Bug fixed: some assert failure were just failures... |
tree | commitdiff |
| 2009-10-19 |
Claudio Sacerdoti... | Smarter implementation of instantiate to avoid re-check... |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | new lambda instros and better logging |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | better indexing for auto |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | some work for auto |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | some work for auto |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | removed optimization potentially unsound |
tree | commitdiff |
| 2009-10-15 |
Claudio Sacerdoti... | Profiling code integrated. |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Debugging improved. |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Benchmarking integrated in folding/unfolding. |
tree | commitdiff |
| 2009-10-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-10-14 |
Enrico Tassi | hints were not used by reduction machines on heads |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Error message fixed (dereferencing must be done eagerly... |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Serious bug fixed: fix_sorts used to allow inference... |
tree | commitdiff |
| 2009-10-14 |
Enrico Tassi | CProp uri fixed |
tree | commitdiff |
| 2009-10-13 |
Enrico Tassi | relocate is hopefully fixed once and for-all! |
tree | commitdiff |
| 2009-10-13 |
Enrico Tassi | relocate fixed |
tree | commitdiff |
| 2009-10-13 |
Enrico Tassi | better ppcontext |
tree | commitdiff |
| 2009-10-13 |
Enrico Tassi | better ppcontext |
tree | commitdiff |
| 2009-10-13 |
Enrico Tassi | debug + relocate uses Prop instead of (Prop Prop).... |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | 1) Bug fixed: the case Meta(i) vs Meta(i) was handled... |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Bug fixed: in case of (t ...) where t has flexible... |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Closed metas must have closed (expected) types. |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Improved debugging code. |
tree | commitdiff |
| 2009-10-12 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-10-11 |
Enrico Tassi | can live without library db |
tree | commitdiff |
| 2009-10-11 |
Enrico Tassi | auto with intro |
tree | commitdiff |
| 2009-10-08 |
Claudio Sacerdoti... | A new switch to activate/deactive nCicReduction pretty... |
tree | commitdiff |
| 2009-10-08 |
Claudio Sacerdoti... | Printing extremely large terms no longer raises Failure. |
tree | commitdiff |
| 2009-10-08 |
Enrico Tassi | removed misleading context |
tree | commitdiff |
| 2009-10-08 |
Enrico Tassi | new discrimination tree instantiation with |
tree | commitdiff |
| 2009-10-08 |
Enrico Tassi | avoid warning |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | removed printing |
tree | commitdiff |
| 2009-10-07 |
Claudio Sacerdoti... | Performance improvement by preserving more sharing... |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | terms indexed in the automation cache are saturated |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | short names |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | auto works on the regular tactics status |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | the wrap function takes a string argument so that we... |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | unfocus can be performed also if all goals are closed |
tree | commitdiff |
| 2009-10-07 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
| 2009-10-07 |
Enrico Tassi | fixed Ref generation |
tree | commitdiff |
| 2009-10-07 |
Claudio Sacerdoti... | - oCic2NCic and nCic2OCic moved to ng_library |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | fixed constructor on non inductive type |
tree | commitdiff |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion: |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | unification pps can be activated by the menu debug |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | nAuto W.I.P. |
tree | commitdiff |
| 2009-10-06 |
Claudio Sacerdoti... | Improved error message. |
tree | commitdiff |
| 2009-10-05 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | auto and auto_paramod are in nAuto |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | new file for auto |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | downcast removed |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | new ng_library module |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | fixed bug in coercion application, input/output swapped... |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | if the query has a completely flexible side, the empty... |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | hints input is cleared from projection redexes |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | projections redex (proj (mk_foo ...)) where mk_foo |
tree | commitdiff |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | better nlet rec boxing |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | Wrong context (again!) |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | - delift_type_wrt_term fixed in many ways |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | fixed the type of tactic_term, attributes were useless |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | instantiate merges tags |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | added sortification for (? args), untested code |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | sortification simplified |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | fixed off-by-one |
tree | commitdiff |
| 2009-09-30 |
Enrico Tassi | rewritten instantiate code |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
tree | commitdiff |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | Better (but still broken) fix for the case ?sort vs... |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | The term contains dummy.conv that was searched over... |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | 1) improved (???) debugging, with |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | Re-indentiation |
tree | commitdiff |
| 2009-09-29 |
Enrico Tassi | ugly coerc db print |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | The unification does not longer use the refiner (urrah!) |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | - fixed bug in coercion application, input/output swapp... |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | 2 lift related bugs fixed! |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | better debug pp |
tree | commitdiff |
| 2009-09-27 |
Enrico Tassi | Type printed as such, CProp printed as such |
tree | commitdiff |
| 2009-09-27 |
Enrico Tassi | fixpoint have attributes for pragma (i.e. they can... |
tree | commitdiff |
| 2009-09-23 |
Enrico Tassi | new macro screenshot |
tree | commitdiff |
| 2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call... |
tree | commitdiff |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
tree | commitdiff |
| 2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types... |
tree | commitdiff |
| next |
projects / helm.git / history