]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 51a0b68) | patch
Bug fixed in assumption_tac: a missing (lift n) when a declaration
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Mar 2005 16:05:54 +0000 (16:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Mar 2005 16:05:54 +0000 (16:05 +0000)
commit0d729d0fb3fd7c798382e16c1f855ce26edad979
tree60164a620092be008e3d0bbe9aa1b73fc24a4271tree | snapshot
parent51a0b68908c1f9ca9cb49f957fb6aae5307674f6commit | diff
Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.
helm/ocaml/tactics/variousTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.