]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f857d0) | patch
bugfix: the function that abstract constant occurrences by putting metavariables
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:04:45 +0000 (09:04 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:04:45 +0000 (09:04 +0000)
commit09cfe0657d77c16be2cc1974cb5242939f1d98fb
tree335acc0706e6a96c5943e64957e6f46a2de1c613tree | snapshot
parent3f857d0acf1872c42ce06238eef793c5e65bc89fcommit | diff
bugfix: the function that abstract constant occurrences by putting metavariables
in place of identity explicit substitutions (local contexts) is generalized to
put ?1 : ?2 : Type in place of a ?1 : Type to take care of <Type in contravariant
position. Note: this is still partially bugged (see previous commit on the same
topic).
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.