]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 78cf601) | patch
CSC: hack to make applications of constants that have a Type sort which
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 24 Mar 2004 16:52:15 +0000 (16:52 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 24 Mar 2004 16:52:15 +0000 (16:52 +0000)
commit62792f5bfe558e6ba0e52e4e51841f4bc02a960a
treed3f0217e85a9f5f33eff556f623e6d3a5d91db47tree | snapshot
parent78cf601fd8b8dbb386b0db315dcbfdbe8256c15fcommit | diff
CSC: hack to make applications of constants that have a Type sort which
occurs in contravariant position work. The idea is to generate in place
of a metavariable of type Type (that should be of type <Type) a
metavariable of type "a metavariable of type Type". The problem is that
in this way the metavariable can also be instantiated that is not a
sort.
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.