| 2009-10-06 |
Enrico Tassi | fixed constructor on non inductive type
|
commit | commitdiff | tree |
| 2009-10-06 |
Enrico Tassi | unification pps can be activated by the menu debug
|
commit | commitdiff | tree |
| 2009-10-06 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-06 |
Enrico Tassi | nAuto W.I.P.
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | auto and auto_paramod are in nAuto
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | new file for auto
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | downcast removed
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | new ng_library module
|
commit | commitdiff | tree |
| 2009-10-05 |
Enrico Tassi | uffa
|
commit | commitdiff | tree |
| 2009-10-02 |
Enrico Tassi | hints fixed
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search