| 2009-07-19 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | nelim now uses the appropriate _rect_XXX elimination... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | 1) the user is notified when a new object is defined |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | More info to refine empty types elimination. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Old code commented out. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Generation of principles is now atomic. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
| 2009-07-17 |
Enrico Tassi | add comment |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Non reproducible. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Some bugs already fixed. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Bugs (mostly from Oliboni) |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Bug fixed: singleton application. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | New suffixes for elimination principles: |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | 1) added a function to retrieve all the universes curre... |
tree | commitdiff |
| 2009-07-17 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Generation of inductive principle for Type[0]. |
tree | commitdiff |
| 2009-07-16 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-16 |
denes | Sorted version of eligible problems list |
tree | commitdiff |
| 2009-07-16 |
denes | Disabled age selection and ad hoc goal weight computation |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to... |
tree | commitdiff |
| 2009-07-15 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code... |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the... |
tree | commitdiff |
| 2009-07-15 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-14 |
denes | Fixed Option type error (OCaml bug) |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-14 |
Cosimo Oliboni | freescale porting to ng, work in progress |
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 |
denes | Added statistics module |
tree | commitdiff |
| 2009-07-13 |
Claudio Sacerdoti... | First proof finished (some tactics still not working). |
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-13 |
Cosimo Oliboni | freescale translation (work in progress) |
tree | commitdiff |
| 2009-07-12 |
Cosimo Oliboni | (no commit message) |
tree | commitdiff |
| 2009-07-11 |
Cosimo Oliboni | (no commit message) |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | Composite coercions are here! |
tree | commitdiff |
| 2009-07-10 |
Ferruccio Guidi | - brgOutput: the nodes count is now implemented |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | more work on coercions composition |
tree | commitdiff |
| 2009-07-10 |
Cosimo Oliboni | +root +depends |
tree | commitdiff |
| 2009-07-10 |
denes | Removed unused parameter of unification procedure ... |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | more profilers |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | Coercions used here and there. |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | Bug fixed (missing ctx) + comment added. |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-10 |
Cosimo Oliboni | new ng freescale, no external dependencies |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | Let's live with new ocaml type system limitations... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | claudio, please have a look at this |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a... |
tree | commitdiff |
| 2009-07-09 |
denes | Fixed check for condition iv p.33 (Riazzanov) |
tree | commitdiff |
| 2009-07-09 |
Wilmer Ricciotti | More updates to Fsub. |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varli... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | 1 process for now |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | micro optimizations to unification |
tree | commitdiff |
| 2009-07-09 |
denes | Cleaned a bit |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | activate kbo, not lpo |
tree | commitdiff |
| 2009-07-09 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-09 |
Claudio Sacerdoti... | Bug fixed (non-captured variable). |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | eq moved to CProp |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | repeat_tac |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-08 |
Enrico Tassi | few more files, one diverges |
tree | commitdiff |
| 2009-07-08 |
Enrico Tassi | removed useless universes |
tree | commitdiff |
| 2009-07-08 |
Enrico Tassi | import of a sample for cosimo |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Hmmmm. This way we need "canonical structures" also... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Metavariable case in does_not_occur (hence weakly/stric... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Missing case for Match implemented. |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | weakly/strictly positive checks relaxed to allow metava... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Improved error message. |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | Bug fixed: one uri was not refreshed, causing divergenc... |
tree | commitdiff |
| 2009-07-07 |
Enrico Tassi | fixed some typos |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | Let's play a bit with NG. |
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-06 |
denes | Tried to implement lpo in a more efficient way |
tree | commitdiff |
| 2009-07-06 |
denes | Fixed typo in lpo (from old implementation) |
tree | commitdiff |
| 2009-07-03 |
Ferruccio Guidi | some corrections |
tree | commitdiff |
| 2009-07-03 |
Ferruccio Guidi | more static analysis on the Automath text |
tree | commitdiff |
| 2009-07-03 |
denes | Ported old implementation of LPO (for test purposes) |
tree | commitdiff |
| 2009-07-03 |
Ferruccio Guidi | we now do some static analysis on the Automath text... |
tree | commitdiff |
| 2009-07-03 |
denes | Implemented LPO |
tree | commitdiff |
| 2009-07-02 |
denes | Corrected type for bag |
tree | commitdiff |
| 2009-07-02 |
denes | New age selection |
tree | commitdiff |
| 2009-07-02 |
Enrico Tassi | better output handling |
tree | commitdiff |
| 2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology |
tree | commitdiff |
| next |
projects / helm.git / history