]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5fe1ee) | patch
Bug fixed that reveals a new one: in case of inductive types defined via
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Feb 2013 20:17:41 +0000 (20:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Feb 2013 20:17:41 +0000 (20:17 +0000)
commitd208b69293abef9a36eb5366d93f6e1ef4c8125e
tree4f34030553d2daaba479ae371915ef2ba1bfcc5atree | snapshot
parentc5fe1eeb2b575d1c696ca15ad9155223839d82e2commit | diff
Bug fixed that reveals a new one: in case of inductive types defined via
let rec, it used to happen that a "type 'a foo" in the .mli was implemented
by a "type 'a foo" in the .ml. Now the opposite happens in other situations.
matita/components/ng_extraction/extraction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.