Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-10 13:33:51 -0700 (Thu, 10 Jul 2008)
Revision: 13107
Log message:
added phase1-2 substitution between families computation (assign) and realization per se (g2h)
the substitution after g2h serves a different purpose - it replaces principla provisionals with terms evaluated in g2h
Changes | Path(relative to metaprl/theories/s4lp) |
+75 -10 | hilbert_internal.ml |