| 2009-07-29 |
Andrea Asperti | Added the benchmark with the new demodulation function. |
tree | commitdiff |
| 2009-07-28 |
denes | New reference benchmark with CPU Time |
tree | commitdiff |
| 2009-07-27 |
denes | Removed internal default timeout |
tree | commitdiff |
| 2009-07-27 |
denes | Removed old logs |
tree | commitdiff |
| 2009-07-27 |
denes | Moved benchmarks to new folder |
tree | commitdiff |
| 2009-07-20 |
denes | Removed status printing by processes |
tree | commitdiff |
| 2009-07-20 |
denes | Fixed multiple printing |
tree | commitdiff |
| 2009-07-20 |
Wilmer Ricciotti | Final version, submitted to CASC-22. |
tree | commitdiff |
| 2009-07-16 |
denes | Sorted version of eligible problems list |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | better spacing |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort |
tree | commitdiff |
| 2009-07-13 |
denes | Added statistics printings |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the comput... |
tree | commitdiff |
| 2009-07-13 |
Claudio Sacerdoti... | Coercion hiding implemented. Notes: |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | 1 process for now |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-07-06 |
denes | Fixed printing of number of problems solved |
tree | commitdiff |
| 2009-07-02 |
denes | Corrected type for bag |
tree | commitdiff |
| 2009-07-02 |
Enrico Tassi | better output handling |
tree | commitdiff |
| 2009-07-01 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-01 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-01 |
Wilmer Ricciotti | Version number set to 1.0.0-rc1 |
tree | commitdiff |
| 2009-07-01 |
denes | Fixed type of bag |
tree | commitdiff |
| 2009-06-30 |
Enrico Tassi | parallel |
tree | commitdiff |
| 2009-06-30 |
Enrico Tassi | attempt of using 2 different orderings |
tree | commitdiff |
| 2009-06-30 |
Enrico Tassi | .... |
tree | commitdiff |
| 2009-06-30 |
denes | Corrected a few typos |
tree | commitdiff |
| 2009-06-30 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-29 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-29 |
Enrico Tassi | new make test target |
tree | commitdiff |
| 2009-06-26 |
Andrea Asperti | the timeout is passed to test last chance |
tree | commitdiff |
| 2009-06-26 |
Andrea Asperti | fixed parsing |
tree | commitdiff |
| 2009-06-26 |
Andrea Asperti | convenient problem lists |
tree | commitdiff |
| 2009-06-26 |
Andrea Asperti | an easy for loop |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | better doc |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | timeouts are passed as arguments, so that tptpprover can |
tree | commitdiff |
| 2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | the prover is almost OK, types in fuctors a bit extended to |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | matitaprover is almost there |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | initial import of standalone matitaprover binary |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (by CSC,actuall :-) |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
tree | commitdiff |
| 2009-06-11 |
Ferruccio Guidi | - some depend files fixed |
tree | commitdiff |
| 2009-06-10 |
Ferruccio Guidi | - library/list/list.ma: unused code commented |
tree | commitdiff |
| 2009-06-09 |
Ferruccio Guidi | - Procedural: more support for the Debug inline option... |
tree | commitdiff |
| 2009-06-06 |
Claudio Sacerdoti... | Previous commit reverted, as explained in that log. |
tree | commitdiff |
| 2009-06-06 |
Claudio Sacerdoti... | This commit restores the ids_to_father_ids table. |
tree | commitdiff |
| 2009-06-05 |
Ferruccio Guidi | - Procedural convertible rewrites in the conclusion... |
tree | commitdiff |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unifica... |
tree | commitdiff |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
tree | commitdiff |
| 2009-05-28 |
Ferruccio Guidi | - cicInspect: relevant nodes count updated: letin nodes... |
tree | commitdiff |
| 2009-05-27 |
Ferruccio Guidi | - Procedural: we specify more unifiers for apply to... |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-05 |
Ferruccio Guidi | - hExtlib: new function "list_assoc_all" |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
tree | commitdiff |
| 2009-04-22 |
Ferruccio Guidi | - transcript: we have now two styles of mma's from... |
tree | commitdiff |
| 2009-04-21 |
Ferruccio Guidi | - MatitaMisc: we factorized here the function out_pream... |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-16 |
Ferruccio Guidi | Procedural: we corrected two errors about the handling... |
tree | commitdiff |
| 2009-04-16 |
Enrico Tassi | Universe is used only locally to tactics/ |
tree | commitdiff |
| 2009-04-15 |
Ferruccio Guidi | - transcript: bugfix |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | - Procedural: generation of "exact" is now complete |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and... |
tree | commitdiff |
| 2009-03-30 |
Enrico Tassi | tentative subst-sexpand and change |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2008-11-30 |
Ferruccio Guidi | lambda-delta/toplevel: improved transformation from... |
tree | commitdiff |
| 2008-11-25 |
Ferruccio Guidi | cicUtil: we moved here pp_term from proceduralHelpers |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | auto was compiraing lazy proof terms with = ... fixed |
tree | commitdiff |
| 2008-09-05 |
Ferruccio Guidi | transcript: we now check for non-existing objects |
tree | commitdiff |
| 2008-09-04 |
Ferruccio Guidi | transcript: improved debuugging facilities |
tree | commitdiff |
| 2008-09-04 |
Ferruccio Guidi | transcript: we improved the parser/lexer to read the... |
tree | commitdiff |
| 2008-08-25 |
Ferruccio Guidi | transcript: bug fix in the generation of axioms |
tree | commitdiff |
| 2008-08-23 |
Ferruccio Guidi | Procedural: explicit flavour specification for constant... |
tree | commitdiff |
| 2008-08-21 |
Ferruccio Guidi | basic support for imposed flavour in procedural object... |
tree | commitdiff |
| 2008-07-22 |
Ferruccio Guidi | matitadep: we now handle the inline of an uri, we remov... |
tree | commitdiff |
| 2008-07-22 |
Ferruccio Guidi | transcript: now we can generate procedural output |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-07-26 |
Ferruccio Guidi | We add a binary for computing the "heights" of helm... |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | map_unicode_to_tex is no longer optional and it always... |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-05-18 |
lzingare | added alternative implementation for hMysql relying |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | now we try two distinct depend files for compilation... |
tree | commitdiff |
| 2006-12-13 |
Ferruccio Guidi | - transcript: patched to generate aliases instead of... |
tree | commitdiff |
| 2006-12-12 |
Ferruccio Guidi | we parametrized CicNotationPt.obj on 'term |
tree | commitdiff |
| 2006-12-12 |
Ferruccio Guidi | we started the infrastructure for the procedural render... |
tree | commitdiff |
| 2006-12-05 |
Ferruccio Guidi | - components: composed coercions mus be generated with... |
tree | commitdiff |
| 2006-11-29 |
Ferruccio Guidi | - decompose tactic: decomposable constants are now... |
tree | commitdiff |
| 2006-11-17 |
Ferruccio Guidi | helm_registry: added the pair unmarshaller |
tree | commitdiff |
| 2006-11-16 |
Ferruccio Guidi | - transcript: patched to generate CoRN_notation.ma... |
tree | commitdiff |
| next |
projects / helm.git / history