]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 513c712) | patch
* Bug fixed: applications of MutCase that are not iota-redexes were reduced
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Apr 2002 09:34:07 +0000 (09:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Apr 2002 09:34:07 +0000 (09:34 +0000)
commitf3d3702d9dae5012484ec7b9afe35c56be73ca5d
tree893dd0e05b3e9ca9d913ec7029760abd75b487f7tree | snapshot
parent513c712655ff11a969ff2eed7f09c3133bc6aec9commit | diff
* Bug fixed: applications of MutCase that are not iota-redexes were reduced
  just to their head.
* More debugging enabled (to be removed when code becomes stable)
helm/ocaml/cic_proof_checking/cicReductionNaif.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.