]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e436c17) | patch
simplify has a brand new semantics!
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Apr 2007 21:15:44 +0000 (21:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Apr 2007 21:15:44 +0000 (21:15 +0000)
commitcd3f9f850d16320dcc8fb1590e1cc9f8ba29e37b
tree124c9114c0291de3a97a4eb63711a87781663f7btree | snapshot
parente436c170ce2b9154d3e090c2140e8a0172f4a016commit | diff
simplify has a brand new semantics!
replace_lifting passes a context to the comparison function
(but in the case Fix/CoFix is incomplete)
helm/software/components/tactics/inversion.ml diff | blob | history
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
helm/software/components/tactics/primitiveTactics.ml diff | blob | history
helm/software/components/tactics/proofEngineReduction.ml diff | blob | history
helm/software/components/tactics/proofEngineReduction.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.