]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5aee2f8) | patch
- double_type_of: sort_of_prod modified to expect also a meta
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 10:48:11 +0000 (10:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 10:48:11 +0000 (10:48 +0000)
commit4495bd142fb9f80b66f712ec8264f97b8ec1c258
tree1d98125741c5c3cdb31b42f11bce9c1c5cf8f498tree | snapshot
parent5aee2f85474686a307f2acda957ffe363a72eff3commit | diff
- double_type_of: sort_of_prod modified to expect also a meta
- cic2acic: string_of_sort badly patched to return a "?" when a meta
  is found. Note: this solution is not admissible, since it generates
  non-valid XML files (and it may also break other things).
helm/ocaml/cic_omdoc/cic2acic.ml diff | blob | history
helm/ocaml/cic_omdoc/doubleTypeInference.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.