- add a patch (by Sam) to have a prove-formula function in PVS
- remove "opaque" keyword because of issue 830 of lambdapi,
- added some encoding facilities to write proofs
- export has a switch to translate proofs

General simplifications

Do not remember types in context anymore

Fix tests (call correct function), fix some newlines printing

Discard pvs2k script, use a lisp function
Discard logging, use trace instead
Discard to-dk3 and rely on pp-dk