| 2009-07-17 | 
Claudio Sacerdoti...  | Non reproducible. | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | Some bugs already fixed. | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | Bugs (mostly from Oliboni) | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | Bug fixed: singleton application. | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | New suffixes for elimination principles: | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | 1) added a function to retrieve all the universes curre...  | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Cosimo Oliboni |  freescale porting, work in progress | 
commit | commitdiff | tree | snapshot | 
| 2009-07-17 | 
Claudio Sacerdoti...  | Generation of inductive principle for Type[0]. | 
commit | commitdiff | tree | snapshot | 
| 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 | 
| next |