| 2008-11-06 |
Enrico Tassi | natural deduction support and example split, seems...
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | do not erase sorts
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | better error messages. sorts are compared using whd
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | Evil case fixed, the coulde should be more readable
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | removed empty lines
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | the passive set and passive list are expected to have...
|
commit | commitdiff | tree |
| 2008-11-06 |
Enrico Tassi | fixed scripts
|
commit | commitdiff | tree |
| 2008-11-05 |
Enrico Tassi | still some glitches, but reaching a decent state
|
commit | commitdiff | tree |
| 2008-11-05 |
Enrico Tassi | using the new by foo we proved semantics
|
commit | commitdiff | tree |
| 2008-11-05 |
Enrico Tassi | new internal flags for auto:
|
commit | commitdiff | tree |
| 2008-11-05 |
Enrico Tassi | duplicate entry in menv avoided
|
commit | commitdiff | tree |
| 2008-11-05 |
Enrico Tassi | fixed script to use auto depth=4
|
commit | commitdiff | tree |
| 2008-11-04 |
Enrico Tassi | eliminazione di un passaggio di transitività in ast2astfe
|
commit | commitdiff | tree |
| 2008-11-03 |
Enrico Tassi | BDD
|
commit | commitdiff | tree |
| 2008-11-03 |
Enrico Tassi | removed prerr_endline
|
commit | commitdiff | tree |
| 2008-11-03 |
Enrico Tassi | debug=false
|
commit | commitdiff | tree |
| 2008-11-02 |
Enrico Tassi | shannon proved
|
commit | commitdiff | tree |
| 2008-11-01 |
Enrico Tassi | added shannon
|
commit | commitdiff | tree |
| 2008-11-01 |
Enrico Tassi | added lazy
|
commit | commitdiff | tree |
| 2008-10-29 |
Enrico Tassi | models ported
|
commit | commitdiff | tree |
| 2008-10-28 |
Enrico Tassi | even more polymorphic dualizer
|
commit | commitdiff | tree |
| 2008-10-28 |
Enrico Tassi | done
|
commit | commitdiff | tree |
| 2008-10-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-28 |
Enrico Tassi | lebesge works
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | WIP
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | many bugs fixed
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | metasenv passed to get_relevance, Metas that stand...
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | WIP
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | _ in place of unused variables
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | Implicit annotationas are now printed
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | seg_u/l were inverted, more work
|
commit | commitdiff | tree |
| 2008-10-27 |
Enrico Tassi | big lemma done
|
commit | commitdiff | tree |
| 2008-10-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-26 |
Enrico Tassi | duality done
|
commit | commitdiff | tree |
| 2008-10-26 |
Enrico Tassi | almost done, just needs to be prforated
|
commit | commitdiff | tree |
| 2008-10-26 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2008-10-26 |
Enrico Tassi | all done in declarative style
|
commit | commitdiff | tree |
| 2008-10-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-25 |
Enrico Tassi | duality is a joke
|
commit | commitdiff | tree |
| 2008-10-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-24 |
Enrico Tassi | leave-environment axiom made true
|
commit | commitdiff | tree |
| 2008-10-23 |
Enrico Tassi | lebesgue completely dualized
|
commit | commitdiff | tree |
| 2008-10-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-21 |
Enrico Tassi | better pps
|
commit | commitdiff | tree |
| 2008-10-21 |
Enrico Tassi | - mk_restricted_irl removed, the non-optimized code...
|
commit | commitdiff | tree |
| 2008-10-21 |
Enrico Tassi | psubst for metas fixed again
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | nat model ported to the dualized version, but not itself...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ... is a command in proof mode, use
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | more bug fixed (or introduced)
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | after a PITA, lebergue is dualized!
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | some work on duality, still not finisched
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | grave notation mistake fixed
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | more tests
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-19 |
Enrico Tassi | when a file is opened the cursor is moved to the begin...
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | tactic language documented;
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | html documentation generation implemented
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | more doc
|
commit | commitdiff | tree |
| 2008-10-18 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-17 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-17 |
Enrico Tassi | new command eval added
|
commit | commitdiff | tree |
| 2008-10-17 |
Enrico Tassi | better makefile
|
commit | commitdiff | tree |
| 2008-10-17 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-16 |
Enrico Tassi | ex for students about induction
|
commit | commitdiff | tree |
| 2008-10-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-15 |
Enrico Tassi | delifting a Meta with an IRL w.r.t. another IRL completely...
|
commit | commitdiff | tree |
| 2008-10-15 |
Enrico Tassi | some bug fixed
|
commit | commitdiff | tree |
| 2008-10-15 |
Enrico Tassi | subst_meta was missing
|
commit | commitdiff | tree |
| 2008-10-14 |
Enrico Tassi | more work
|
commit | commitdiff | tree |
| 2008-10-14 |
Enrico Tassi | firs step for dualization
|
commit | commitdiff | tree |
| 2008-10-14 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported...
|
commit | commitdiff | tree |
| 2008-10-13 |
Enrico Tassi | initial refiner ....
|
commit | commitdiff | tree |
| 2008-10-13 |
Enrico Tassi | bug in psubst fixed inside local context in Irl form
|
commit | commitdiff | tree |
| 2008-10-13 |
Enrico Tassi | better error message
|
commit | commitdiff | tree |
| 2008-10-13 |
Enrico Tassi | ppmetasenv & subst added
|
commit | commitdiff | tree |
| 2008-10-13 |
Enrico Tassi | NCicReduction.reduce_machine returns a boolean stating...
|
commit | commitdiff | tree |
| 2008-10-06 |
Enrico Tassi | slow example
|
commit | commitdiff | tree |
| 2008-10-06 |
Enrico Tassi | 3 nasty bugs fixed:
|
commit | commitdiff | tree |
| 2008-10-06 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | better test
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | not so nice patch to small_delta_step
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | when -debug do not catch the exception
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | - NCicPp.ppterm applies the substitution
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | the iterator was wrongly processing the application
|
commit | commitdiff | tree |
| 2008-10-03 |
Enrico Tassi | better debuggin output
|
commit | commitdiff | tree |
| 2008-10-02 |
Enrico Tassi | error...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search