]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9fa9ed) | patch
lazily ==> call_by_name (since it is really a call_by_name!)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Nov 2002 17:25:51 +0000 (17:25 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Nov 2002 17:25:51 +0000 (17:25 +0000)
commit9d35b4005007408a49a76864302f03db8aa7789a
tree96fd2a1db5d152e8e69df50a09b7f286c9c4faabtree | snapshot
parente9fa9ed4a406a66a1955bfd7ec4e0f76cec15eb3commit | diff
lazily ==> call_by_name (since it is really a call_by_name!)

The default is now false (i.e. call_by_value strategy) to make an example
of Fourier application type-check in 8s instead of 1h40m!!!

We also tried a call_by_need strategy (not committed).
The results obtained are so far equivalent to the call_by_value strategy
(that is why we did not commit the code).
helm/ocaml/cic_proof_checking/cicReductionMachine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.