Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 04:25:13 -0800 (Fri, 21 Mar 2003)
Revision: 4206
Log message:
*** WARNING ***
*** This check-in breaks .prlb compatibility ***
*** Export any unsaved proofs to .prla ***
*** before running "cvs update" ***
- I have added support for Hypothesis that do not introduce a binding variable.
I do not yet have much I/O support for them - there is no mechanism yet for
inputing such hypotheses explicitly and the display format for them is not
ideal. I will add this later.
Note:
1) A hypothesis with an unused binding and a hypothesis without a binding are
considered equivalent (e.g. in alpha equality comparisons).
2) All the sequents on _rule box_ level are normalized. When a sequent is normalized,
all the binding hyps that introduce an unused variable a changed to non-binding ones
(ideally - for some reason it does yet not always work correctly).
3) If you want to give a name to a no-name variable, use nameHypT or nameHypsT tactic.
Note that you have to use that name right away in the _same_ rulebox, otherwise
normalization (see note 2) will remove it again!
I plan to extend nameHypT/nameHypsT to be able to rename existing bindings as well,
but have not done that yet.
- I have changed the way variable names are handled in the rewriter - now it
will watch them much more carefully, most of the bugs related to the variable
names are fixed (but a few still remain).
- I fixed all the proofs these changes broke (there were quite a few), except for
/itt_record/recordEliminationL
- vnewname: now "v_1" would be renamed into "v_2", not "v_1_1"
- I bumped MetaPRL version number to 0.8
- I bumped the ASCII version number to 1.0.1 (it will still read the old 1.0.0,
but will correctly mark all new .prla as 1.0.1 which will prevent the old MetaPRL
from thinking it can read them)
- I changed the magic numbers for .prlb (or at least I hope I did it correctly), so
hopefully it will ignore any old .prlb you might have and not crash on them.