]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3af4c2) | patch
* (Head) beta reduction functions factorized
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Jun 2005 14:03:41 +0000 (14:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Jun 2005 14:03:41 +0000 (14:03 +0000)
commited9af5a10b66343f817a1f9eac3add29e4b2baae
treed424e003163ce7a810cd28f2abac006fc38df5b7tree | snapshot
parentd3af4c289c9870337a141a0ffa98f9e01439d806commit | diff
* (Head) beta reduction functions factorized
* the type inferred for a match both in the kernel and in the refiner
  are now beta reduced
helm/ocaml/cic_proof_checking/cicReduction.ml diff | blob | history
helm/ocaml/cic_proof_checking/cicReduction.mli diff | blob | history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
helm/ocaml/cic_unification/cicMetaSubst.ml diff | blob | history
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.