| 2009-09-11 |
Enrico Tassi | constructor accepts the arguments of the constructor...
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | new tactic constructor: @[n]
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | new syntax
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | let rec/corec and co/inductive are not printed!
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | new macro ncheck. fixed term2pres for Inductive and...
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | ok, but slow on includes
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | nice hints
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | maledetto il \sub di CSC
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | it starts to work
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | nice notation for hints!
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | allow @{ ... } as the identifier of the letin
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | to me, the problem:
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | more stuff fixed
|
commit | commitdiff | tree |
| 2009-09-10 |
Enrico Tassi | the refiner was not checking that the resulting type
|
commit | commitdiff | tree |
| 2009-09-09 |
Enrico Tassi | some fixes here and there
|
commit | commitdiff | tree |
| 2009-09-09 |
Enrico Tassi | depends
|
commit | commitdiff | tree |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions
|
commit | commitdiff | tree |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC
|
commit | commitdiff | tree |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC
|
commit | commitdiff | tree |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing):
|
commit | commitdiff | tree |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing):
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | fix to speedup reduction making intermediate conversion...
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | fixed eliminator name
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | some work
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | CIC has no eta-reduction/expansion
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | do not fail if the inductive type is mutual, just do...
|
commit | commitdiff | tree |
| 2009-09-02 |
Enrico Tassi | decent error on interpretation declaration
|
commit | commitdiff | tree |
| 2009-09-01 |
Enrico Tassi | fix double app in Ast
|
commit | commitdiff | tree |
| 2009-09-01 |
Enrico Tassi | better print of ILLEGAL applications
|
commit | commitdiff | tree |
| 2009-09-01 |
Enrico Tassi | catch wrapped exception
|
commit | commitdiff | tree |
| 2009-08-28 |
Enrico Tassi | alias bug revealed
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | initial and incomplete port of the old demo about inductivel...
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | exponentiation should output with \sup not with ^,...
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | added "already defined"
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | ncoindutive now generates a co-inductive type, not...
|
commit | commitdiff | tree |
| 2009-08-25 |
Enrico Tassi | Meta case not handled, the iterator was complaining.
|
commit | commitdiff | tree |
| 2009-07-20 |
Enrico Tassi | sorted modules
|
commit | commitdiff | tree |
| 2009-07-17 |
Enrico Tassi | add comment
|
commit | commitdiff | tree |
| 2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to...
|
commit | commitdiff | tree |
| 2009-07-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the...
|
commit | commitdiff | tree |
| 2009-07-13 |
Enrico Tassi | better spacing
|
commit | commitdiff | tree |
| 2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort
|
commit | commitdiff | tree |
| 2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the computation...
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | more work on coercions composition
|
commit | commitdiff | tree |
| 2009-07-10 |
Enrico Tassi | more profilers
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | claudio, please have a look at this
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varlist...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | 1 process for now
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | micro optimizations to unification
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-09 |
Enrico Tassi | activate kbo, not lpo
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | few more files, one diverges
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | removed useless universes
|
commit | commitdiff | tree |
| 2009-07-08 |
Enrico Tassi | import of a sample for cosimo
|
commit | commitdiff | tree |
| 2009-07-07 |
Enrico Tassi | fixed some typos
|
commit | commitdiff | tree |
| 2009-07-02 |
Enrico Tassi | better output handling
|
commit | commitdiff | tree |
| 2009-07-02 |
Enrico Tassi | return type of paramod fixed according to the SZSOntology
|
commit | commitdiff | tree |
| 2009-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | parallel
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | attempt of using 2 different orderings
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2009-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | do not infer on closed goals
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | removed a maybe diverging test
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | added (but not active) last chance idea
|
commit | commitdiff | tree |
| 2009-06-29 |
Enrico Tassi | new make test target
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | better doc
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | timeouts are passed as arguments, so that tptpprover can
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | the prover is almost OK, types in fuctors a bit extended to
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | new function
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | matitaprover is almost there
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | initial import of standalone matitaprover binary
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | code refactoring for paramodulation
|
commit | commitdiff | tree |
| 2009-06-25 |
Enrico Tassi | new function list_mapi_acc
|
commit | commitdiff | tree |
| 2009-06-23 |
Enrico Tassi | undo/serialization for universes implemented
|
commit | commitdiff | tree |
| 2009-06-23 |
Enrico Tassi | removed problem not in UEQ
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | debug pps removed
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | better exception handling
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | proof patching!
|
commit | commitdiff | tree |
| 2009-06-18 |
Enrico Tassi | callbacks were taking in input a status bu were not...
|
commit | commitdiff | tree |
| 2009-06-17 |
Enrico Tassi | proof reconstruction almost OK
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | first proof reconstruction attempt, still bugged since it
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | avoid fixing non-recursive terms
|
commit | commitdiff | tree |
| 2009-06-16 |
Enrico Tassi | we fix recursive object reference with the correct...
|
commit | commitdiff | tree |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (part B, by CSC :-):
|
commit | commitdiff | tree |
| next |
projects / helm.git / search