2009-07-16 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-16 |
denes | Sorted version of eligible problems list |
commit | commitdiff | tree | snapshot |
2009-07-16 |
denes | Disabled age selection and ad hoc goal weight computation |
commit | commitdiff | tree | snapshot |
2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to... |
commit | commitdiff | tree | snapshot |
2009-07-15 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code... |
commit | commitdiff | tree | snapshot |
2009-07-15 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the... |
commit | commitdiff | tree | snapshot |
2009-07-15 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-14 |
denes | Fixed Option type error (OCaml bug) |
commit | commitdiff | tree | snapshot |
2009-07-14 |
denes | . |
commit | commitdiff | tree | snapshot |
2009-07-14 |
denes | . |
commit | commitdiff | tree | snapshot |
2009-07-14 |
Cosimo Oliboni | freescale porting to ng, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Enrico Tassi | better spacing |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort |
commit | commitdiff | tree | snapshot |
2009-07-13 |
denes | Added statistics printings |
commit | commitdiff | tree | snapshot |
2009-07-13 |
denes | Added statistics module |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Claudio Sacerdoti... | First proof finished (some tactics still not working). |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the comput... |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Claudio Sacerdoti... | Coercion hiding implemented. Notes: |
commit | commitdiff | tree | snapshot |
2009-07-13 |
Cosimo Oliboni | freescale translation (work in progress) |
commit | commitdiff | tree | snapshot |
2009-07-12 |
Cosimo Oliboni | (no commit message) |
commit | commitdiff | tree | snapshot |
2009-07-11 |
Cosimo Oliboni | (no commit message) |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Claudio Sacerdoti... | Composite coercions are here! |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Ferruccio Guidi | - brgOutput: the nodes count is now implemented |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Enrico Tassi | more work on coercions composition |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Cosimo Oliboni | +root +depends |
commit | commitdiff | tree | snapshot |
2009-07-10 |
denes | Removed unused parameter of unification procedure ... |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Enrico Tassi | more profilers |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Claudio Sacerdoti... | Coercions used here and there. |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Claudio Sacerdoti... | Bug fixed (missing ctx) + comment added. |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Cosimo Oliboni | new ng freescale, no external dependencies |
commit | commitdiff | tree | snapshot |
2009-07-10 |
Claudio Sacerdoti... | Let's live with new ocaml type system limitations... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | claudio, please have a look at this |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
denes | Fixed check for condition iv p.33 (Riazzanov) |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Wilmer Ricciotti | More updates to Fsub. |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varli... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | 1 process for now |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | micro optimizations to unification |
commit | commitdiff | tree | snapshot |
2009-07-09 |
denes | Cleaned a bit |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Enrico Tassi | activate kbo, not lpo |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-09 |
Claudio Sacerdoti... | Bug fixed (non-captured variable). |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | eq moved to CProp |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | repeat_tac |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Enrico Tassi | few more files, one diverges |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Cosimo Oliboni | directory for porting the assembly to matita-ng |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Enrico Tassi | removed useless universes |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Enrico Tassi | import of a sample for cosimo |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | Hmmmm. This way we need "canonical structures" also... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | Metavariable case in does_not_occur (hence weakly/stric... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | Missing case for Match implemented. |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | weakly/strictly positive checks relaxed to allow metava... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | Improved error message. |
commit | commitdiff | tree | snapshot |
2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
commit | commitdiff | tree | snapshot |
2009-07-07 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-07 |
Claudio Sacerdoti... | Bug fixed: one uri was not refreshed, causing divergenc... |
commit | commitdiff | tree | snapshot |
2009-07-07 |
Enrico Tassi | fixed some typos |
commit | commitdiff | tree | snapshot |
2009-07-07 |
Claudio Sacerdoti... | Let's play a bit with NG. |
commit | commitdiff | tree | snapshot |
2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
commit | commitdiff | tree | snapshot |
2009-07-06 |
denes | Fixed printing of number of problems solved |
commit | commitdiff | tree | snapshot |
2009-07-06 |
denes | Tried to implement lpo in a more efficient way |
commit | commitdiff | tree | snapshot |
2009-07-06 |
denes | Fixed typo in lpo (from old implementation) |
commit | commitdiff | tree | snapshot |
2009-07-03 |
Ferruccio Guidi | some corrections |
commit | commitdiff | tree | snapshot |
2009-07-03 |
Ferruccio Guidi | more static analysis on the Automath text |
commit | commitdiff | tree | snapshot |
2009-07-03 |
denes | Ported old implementation of LPO (for test purposes) |
commit | commitdiff | tree | snapshot |
2009-07-03 |
Ferruccio Guidi | we now do some static analysis on the Automath text... |
commit | commitdiff | tree | snapshot |
2009-07-03 |
denes | Implemented LPO |
commit | commitdiff | tree | snapshot |
2009-07-02 |
denes | Corrected type for bag |
commit | commitdiff | tree | snapshot |
2009-07-02 |
denes | New age selection |
commit | commitdiff | tree | snapshot |
2009-07-02 |
Enrico Tassi | better output handling |
commit | commitdiff | tree | snapshot |
2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology |
commit | commitdiff | tree | snapshot |
2009-07-01 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-07-01 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-07-01 |
Wilmer Ricciotti | Version number set to 1.0.0-rc1 |
commit | commitdiff | tree | snapshot |
2009-07-01 |
denes | Fixed type of bag |
commit | commitdiff | tree | snapshot |
2009-06-30 |
Enrico Tassi | parallel |
commit | commitdiff | tree | snapshot |
2009-06-30 |
denes | Moved ID management inside the bag |
commit | commitdiff | tree | snapshot |
2009-06-30 |
Enrico Tassi | attempt of using 2 different orderings |
commit | commitdiff | tree | snapshot |
2009-06-30 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2009-06-30 |
denes | Corrected a few typos |
commit | commitdiff | tree | snapshot |
2009-06-30 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-06-30 |
denes | Enabled age selection (ratio 1/5) |
commit | commitdiff | tree | snapshot |
2009-06-29 |
Ferruccio Guidi | lambda-delta: |
commit | commitdiff | tree | snapshot |
2009-06-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-06-29 |
Enrico Tassi | do not infer on closed goals |
commit | commitdiff | tree | snapshot |
2009-06-29 |
Enrico Tassi | removed a maybe diverging test |
commit | commitdiff | tree | snapshot |
2009-06-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
next |