]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5606235) | patch
added apply_tac_verbose_with_subst, returning a Cic.substitution instead of a
authorAlberto Griggio <griggio@fbk.eu>
Mon, 26 Sep 2005 14:55:28 +0000 (14:55 +0000)
committerAlberto Griggio <griggio@fbk.eu>
Mon, 26 Sep 2005 14:55:28 +0000 (14:55 +0000)
commit04ade947888ac1115dfe104714bed61c32e1c9c3
tree76e2fd2a59bc8e1c68bd739e5a34e2cd01fd0cf0tree | snapshot
parent56062350e31144f05421de6f895101ab3defc324commit | diff
added apply_tac_verbose_with_subst, returning a Cic.substitution instead of a
substitution function, needed by the new paramodulation
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
helm/ocaml/tactics/primitiveTactics.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.