Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 12:57:46 -0700 (Fri, 26 May 2000)
Revision: 2993
Log message:
- Fixed a nasty bug in Term_ds.subst - it didn't notice when the same variable
was mentioned several times in the substitution with different terms substituted
for it. This made it possible to break Term_ds invariants leading to all kinds of
strange behaviour.
- Changed the argument order for "subst" to be more natural
- Added a subst1 function to substitute for a single variable without having
to put the substitution into a singleton list.
- Added the resource annotations and updated the rest of the resource code
in CZF so that it now compiles (but I didn't try to expand anything).