]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d556d11) | patch
Computed inner-types are now also put in whd normal form.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Apr 2002 10:22:09 +0000 (10:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Apr 2002 10:22:09 +0000 (10:22 +0000)
commit2a40efede6d4430b4ca086275bcac80905ec1a74
treeba0b6e0f8608dca52899a3987ec34e2c0ff6cd85tree | snapshot
parentd556d11bb205b101c9dfa20f35fdd1b0be1ae3a8commit | diff
Computed inner-types are now also put in whd normal form.
This is at the same type too strong (e.g. it performs delta-reductions)
and too weak (it is not full-reduction).
We can consider this just a patch waiting for Coscoy's double-inference
algorithm implementation.
helm/gTopLevel/cic2acic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.