| 2009-10-12 |
Enrico Tassi | added last 10 months work...
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | new standard library inside path
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-11 |
Enrico Tassi | no need to compile/install the standard library. if...
|
commit | commitdiff | tree |
| 2009-10-11 |
Enrico Tassi | can live without library db
|
commit | commitdiff | tree |
| 2009-10-11 |
Enrico Tassi | auto with intro
|
commit | commitdiff | tree |
| 2009-10-08 |
Enrico Tassi | removed misleading context
|
commit | commitdiff | tree |
| 2009-10-08 |
Enrico Tassi | new discrimination tree instantiation with
|
commit | commitdiff | tree |
| 2009-10-08 |
Enrico Tassi | avoid warning
|
commit | commitdiff | tree |
| 2009-10-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | removed printing
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | terms indexed in the automation cache are saturated
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | short names
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | auto works on the regular tactics status
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | the wrap function takes a string argument so that we...
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | unfocus can be performed also if all goals are closed
|
commit | commitdiff | tree |
| 2009-10-07 |
Enrico Tassi | fixed Ref generation
|
commit | commitdiff | tree |
| 2009-10-06 |
Enrico Tassi | removed useless stuff
|
commit | commitdiff | tree |
| 2009-10-06 |
Enrico Tassi | some fixes
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search