]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0663e73) | patch
added a subtle List.rev that makes the order of the equalities taken from the library...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 2 Oct 2006 15:33:24 +0000 (15:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 2 Oct 2006 15:33:24 +0000 (15:33 +0000)
commit07d169f337cdb5dffcf2d508c1bac791a60b38d7
treed5fd381fab0fb41ddbbaf4c3c6efaca755d4eec2tree | snapshot
parent0663e736012a6bf2af56758181252289e79352d2commit | diff
added a subtle List.rev that makes the order of the equalities taken from the library as it used to be. In this way the applys test works, but is not clear why the other order does not produce a solution in decent time
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.