30 Mai
2020
30 Mai
'20
20:23
+ let lp = lexp_lexp' (try OL.lexp_whnf lsort (ectx_to_lctx ctx)
I suspect that many/most calls to `OL.lexp_whnf` will want to pass the result through `lexp_lexp'` before using it, so we could/should either change `OL.lexp_whnf` so it always passes its result through `lexp_lexp'`, or provide two variants of `OL.lexp_whnf` one returning a `lexp` and the other returning lexp'`. Stefan