diff options
| author | Hugo Herbelin | 2015-10-04 22:17:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:05 +0100 |
| commit | e7c38a5516246b751b89535594075f6f95a243fd (patch) | |
| tree | d48c0510705e7e2207998d6b2d77d30c5076a60d /kernel/cemitcodes.ml | |
| parent | 650ed1278160c2d6dae7914703c8755ab54e095c (diff) | |
RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local
context for discharge in global declarations. Discharge now done on a
global declaration. Hence removed Def and Assum which were only
partially used (e.g. in rules Def and Assum but not in
delta-conversion, nor in rule Const).
Added discharge rule over definitions using let-in. It replaces the
"substitution" rule since about 7.0.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions