]> matita.cs.unibo.it Git - helm.git/commit
Complete beta reduction added to avoid strange case of deep beta-redexes
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 24 Jul 2003 14:06:03 +0000 (14:06 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 24 Jul 2003 14:06:03 +0000 (14:06 +0000)
commit854ab91c9da5a87346c28a25d9a410f5dc85d15d
tree3b36c4a621b4fff63cefbbc3e2db92918988a2be
parent49d5e4fbf175050e4afdf26494eec5231c0eac8d
Complete beta reduction added to avoid strange case of deep beta-redexes
in the expected types of application heads.
helm/ocaml/cic_omdoc/doubleTypeInference.ml