| 2006-08-24 |
Ferruccio Guidi | - new legature == for \equiv used in the notation for... |
tree | commitdiff |
| 2006-08-01 |
Stefano Zacchiroli | - added a label_of_uri function to easily change node... |
tree | commitdiff |
| 2006-07-27 |
Claudio Sacerdoti... | More debugging output on stderr. |
tree | commitdiff |
| 2006-07-27 |
maiorino | Automation enabled for declarative proofs. Cool. |
tree | commitdiff |
| 2006-07-27 |
maiorino | "that is equivalent to" and "or equivalently" implement... |
tree | commitdiff |
| 2006-07-27 |
maiorino | All the declarative tactics now have a more or less... |
tree | commitdiff |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination... |
tree | commitdiff |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and... |
tree | commitdiff |
| 2006-07-27 |
Claudio Sacerdoti... | print_endline => prerr_endline |
tree | commitdiff |
| 2006-07-26 |
Claudio Sacerdoti... | Patch to the unification to make the case (i l) vs... |
tree | commitdiff |
| 2006-07-26 |
Claudio Sacerdoti... | Debug code commented out. |
tree | commitdiff |
| 2006-07-26 |
Claudio Sacerdoti... | Elim now performs whd to find the inductive type. |
tree | commitdiff |
| 2006-07-26 |
Enrico Tassi | order is important |
tree | commitdiff |
| 2006-07-24 |
Andrea Asperti | Bug fixed: a symbol alias Symb(s,0) now subsumes the... |
tree | commitdiff |
| 2006-07-24 |
Claudio Sacerdoti... | Disambiguation passes simplified. |
tree | commitdiff |
| 2006-07-24 |
Stefano Zacchiroli | use the new graphviz pretty printer API |
tree | commitdiff |
| 2006-07-24 |
Enrico Tassi | added timeout parameter to auto paramodulation. |
tree | commitdiff |
| 2006-07-24 |
Enrico Tassi | more work on matitaprover (no more XML and buris are... |
tree | commitdiff |
| 2006-07-23 |
Enrico Tassi | see BOO025-1 as an example of failure if (mot p) is... |
tree | commitdiff |
| 2006-07-22 |
Enrico Tassi | matitaprover |
tree | commitdiff |
| 2006-07-21 |
Enrico Tassi | eta_fix default to false |
tree | commitdiff |
| 2006-07-20 |
Claudio Sacerdoti... | Revert of the previous situation: when an identifier... |
tree | commitdiff |
| 2006-07-20 |
Enrico Tassi | trans chains even inside letins body |
tree | commitdiff |
| 2006-07-20 |
Stefano Zacchiroli | avoid collapsing node that does not need to be, i.e.: |
tree | commitdiff |
| 2006-07-20 |
Enrico Tassi | removed abstractios for dummy metavariables when genera... |
tree | commitdiff |
| 2006-07-20 |
Stefano Zacchiroli | bugfix: proper computation of the amount of new node... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | New module to extract from the Db direct and inverse... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | exported position_prefix (so that it can be looked... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | use double quotes around escaped URIs, single quotes... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | - enable header to output graphs attributes and graph... |
tree | commitdiff |
| 2006-07-19 |
Claudio Sacerdoti... | Bug fixed in rewrite in multiple hypothesis and/or... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | - added sql statements for querying forward and backwar... |
tree | commitdiff |
| 2006-07-19 |
Stefano Zacchiroli | added sets of uri pairs (useful for edges between uris) |
tree | commitdiff |
| 2006-07-19 |
Claudio Sacerdoti... | is_empty_listing fixed: the ls method normalizes away... |
tree | commitdiff |
| 2006-07-19 |
Claudio Sacerdoti... | Serious bug fixed in simplify: sometimes terms wwere... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | head_beta_reduce can now optionally perform delta reduc... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | Unification improved to handle beta-delta conversion... |
tree | commitdiff |
| 2006-07-18 |
Stefano Zacchiroli | added split_nth |
tree | commitdiff |
| 2006-07-18 |
Stefano Zacchiroli | double quotes node identifiers |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | Quick&dirty patch to make Http_getter_storage.is_empty... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | dependeciesParsed fixed to parse URIs also in QSTRINGs |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | rmdir_descend now works also on non existent dirs |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | magic number incremented (because of the new declarativ... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | libraryclean fixed to eradicate files generated from... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | The dependencies parser is more robust w.r.t. to lexing... |
tree | commitdiff |
| 2006-07-14 |
Andrea Asperti | Added the computation of max_weight for equations in... |
tree | commitdiff |
| 2006-07-13 |
Stefano Zacchiroli | added $Id$ |
tree | commitdiff |
| 2006-07-13 |
Stefano Zacchiroli | use the graphviz pretty printer to generate graphviz... |
tree | commitdiff |
| 2006-07-13 |
Stefano Zacchiroli | moved graphviz pretty printer outside matita, so that... |
tree | commitdiff |
| 2006-07-12 |
Stefano Zacchiroli | generate dot files with attributes on nodes (instead... |
tree | commitdiff |
| 2006-07-12 |
Stefano Zacchiroli | added uri_of_carr |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | Missing copyright added to tactics/declarative.ml* |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Quit (unused) removed. |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Print (unused) removed. |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Search_pat and GrafiteAst.Search_term (both... |
tree | commitdiff |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof... |
tree | commitdiff |
| 2006-07-11 |
Enrico Tassi | - removed Positive and Negative (all is positive) |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | ... |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | improved coercions support: |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | fixed 1,2: and *: according to the camera ready semantics |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | added flatten_map |
tree | commitdiff |
| 2006-07-06 |
Enrico Tassi | fixed *: and n,m: |
tree | commitdiff |
| 2006-07-05 |
Enrico Tassi | bugfix to developments: |
tree | commitdiff |
| 2006-07-03 |
Enrico Tassi | - patch to consider the symbols of the goal when comput... |
tree | commitdiff |
| 2006-06-30 |
Enrico Tassi | pretty proofs are back |
tree | commitdiff |
| 2006-06-29 |
Andrea Asperti | Cleaning up; removed a couple of "open". |
tree | commitdiff |
| 2006-06-29 |
Claudio Sacerdoti... | Demodulate used to be a reduction_kind and it used... |
tree | commitdiff |
| 2006-06-29 |
Claudio Sacerdoti... | WORK IN PROGRESS: |
tree | commitdiff |
| 2006-06-29 |
Enrico Tassi | before goals are inferred with current, |
tree | commitdiff |
| 2006-06-29 |
Enrico Tassi | goals after a superposition step are relocated |
tree | commitdiff |
| 2006-06-28 |
Ferruccio Guidi | - "linear" flag added to lapply (automatic clearing) |
tree | commitdiff |
| 2006-06-28 |
Enrico Tassi | karma: every term the rewrite acts on must be substututed |
tree | commitdiff |
| 2006-06-28 |
Enrico Tassi | superposition_left not performed if the input goal... |
tree | commitdiff |
| 2006-06-27 |
Ferruccio Guidi | - decompose now runs with no arguments (operates on... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed infer_goal, added simplification before inferring... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | using the new metadataConstraint function |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | used the new metadataConstraint function to retrieve... |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed equalities_for_goal |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | the old compute_eq_weight is back (no more max) |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | fixed generation of letins |
tree | commitdiff |
| 2006-06-27 |
Enrico Tassi | added a metas_of_term implemented using sets instead... |
tree | commitdiff |
| 2006-06-26 |
Enrico Tassi | more work for the generic auto parameters |
tree | commitdiff |
| 2006-06-21 |
Enrico Tassi | added the geniric |
tree | commitdiff |
| 2006-06-20 |
Ferruccio Guidi | - fwd concrete syntax fixed |
tree | commitdiff |
| 2006-06-20 |
Enrico Tassi | garbage collection of dead equalities implemented |
tree | commitdiff |
| 2006-06-20 |
Ferruccio Guidi | - added some documentation on the fwd tatcic |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | typo cpying the formal semantic |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | reorganized guiven_clause to work with the on_the_fly... |
tree | commitdiff |
| 2006-06-19 |
Enrico Tassi | demodulation of goal activated again. |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | some experiments |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | added (but still unused) remove_local_context |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | added (but not yet used) remove_local_context |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | Utils.compare_terms instead of compare_weights |
tree | commitdiff |
| 2006-06-19 |
Andrea Asperti | occur_check and unification fixed. now Meta(i,[]) and... |
tree | commitdiff |
| 2006-06-18 |
Enrico Tassi | - some fixes regarding URIs of equality that now should... |
tree | commitdiff |
| 2006-06-18 |
Enrico Tassi | instead of including library_notation we include logic... |
tree | commitdiff |
| 2006-06-16 |
Enrico Tassi | ancient bug solved. if the term is (eq TY A B) the... |
tree | commitdiff |
| 2006-06-16 |
Enrico Tassi | some more on equalities |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added! |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | added applyS |
tree | commitdiff |
| next |
projects / helm.git / history