]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d28e499) | patch
Big bug spotted and commented: the delift function considers the explicit
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 17 Dec 2003 11:49:58 +0000 (11:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 17 Dec 2003 11:49:58 +0000 (11:49 +0000)
commit36ffad7c7847e28c3275897547a7308929748455
tree2b2f6dfe22f28b6c756a95c215ae9a84db9c3d66tree | snapshot
parentd28e499e10fda9fca6cd7767822f018aa2d5950dcommit | diff
Big bug spotted and commented: the delift function considers the explicit
substitution over metavariable occurrences as telescopic. Instead it is
simultaneous.
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.