Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 19:05:06 -0700 (Tue, 08 Jul 2003)
Revision: 4719
Log message:
- Removed the MVar parameter. Now the semantics of the variable parameters (Var)
is the following:
a) In the formal (AKA "Strict") mode, users are not allowed to mention variable
parameters explicitly - at all.
b) In the informal (AKA "Relaxed" or "display") mode, variable parameters are
meta-parameters. But if a contractum has a variable parameter that is not present
in the redices, then it is taken literally (e.g., as a constant).
- In the rewriting stack matching (used only for ML display forms), separated
the concrete/meta distinction for parameters from the destinction between the
different kinds of rewrite stack entries. This makes it easy (and natural) to
write ML display forms that distinquish between paramerers and meta-parameters.
- Fixed the proofs that used to rely on distinction between `v1 and `v_1