| 2009-10-02 |
Enrico Tassi | fixed bug in coercion application, input/output swapped...
|
commit | commitdiff | tree |
| 2009-10-02 |
Enrico Tassi | if the query has a completely flexible side, the empty...
|
commit | commitdiff | tree |
| 2009-10-02 |
Enrico Tassi | hints input is cleared from projection redexes
|
commit | commitdiff | tree |
| 2009-10-02 |
Enrico Tassi | projections redex (proj (mk_foo ...)) where mk_foo
|
commit | commitdiff | tree |
| 2009-10-02 |
Enrico Tassi | better nlet rec boxing
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | - delift_type_wrt_term fixed in many ways
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | fixed the type of tactic_term, attributes were useless
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | instantiate merges tags
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | added sortification for (? args), untested code
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | sortification simplified
|
commit | commitdiff | tree |
| 2009-10-01 |
Enrico Tassi | fixed off-by-one
|
commit | commitdiff | tree |
| 2009-09-30 |
Enrico Tassi | rewritten instantiate code
|
commit | commitdiff | tree |
| 2009-09-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-29 |
Enrico Tassi | ugly coerc db print
|
commit | commitdiff | tree |
| 2009-09-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-29 |
Enrico Tassi | more virtuals
|
commit | commitdiff | tree |
| 2009-09-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-28 |
Enrico Tassi | non ho resistito!
|
commit | commitdiff | tree |
| 2009-09-28 |
Enrico Tassi | - fixed bug in coercion application, input/output swapped...
|
commit | commitdiff | tree |
| 2009-09-28 |
Enrico Tassi | 2 lift related bugs fixed!
|
commit | commitdiff | tree |
| 2009-09-28 |
Enrico Tassi | better debug pp
|
commit | commitdiff | tree |
| 2009-09-27 |
Enrico Tassi | Type printed as such, CProp printed as such
|
commit | commitdiff | tree |
| 2009-09-27 |
Enrico Tassi | fixpoint have attributes for pragma (i.e. they can...
|
commit | commitdiff | tree |
| 2009-09-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | multi screenshot
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | ncheck works in the current ctx
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-24 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | more on screenshot
|
commit | commitdiff | tree |
| 2009-09-23 |
Enrico Tassi | new macro screenshot
|
commit | commitdiff | tree |
| 2009-09-22 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-09-21 |
Enrico Tassi | new tactics by CSC
|
commit | commitdiff | tree |
| 2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call...
|
commit | commitdiff | tree |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes:
|
commit | commitdiff | tree |
| 2009-09-17 |
Enrico Tassi | one more exception printed
|
commit | commitdiff | tree |
| 2009-09-17 |
Enrico Tassi | more work for igft
|
commit | commitdiff | tree |
| 2009-09-16 |
Enrico Tassi | more notation for topologies, and some prentheses that...
|
commit | commitdiff | tree |
| 2009-09-16 |
Enrico Tassi | some more work...
|
commit | commitdiff | tree |
| 2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries.
|
commit | commitdiff | tree |
| 2009-09-14 |
Enrico Tassi | fixed coercion mechanism w.r.t. undo/require
|
commit | commitdiff | tree |
| 2009-09-13 |
Enrico Tassi | a nice bug in meta handling is not visible... brr...
|
commit | commitdiff | tree |
| 2009-09-13 |
Enrico Tassi | some more letters
|
commit | commitdiff | tree |
| 2009-09-11 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search