]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aff6791) | 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)
commit549c0abf3f9d170db297a8b9d35bf4bf97288662
tree4e26477591e19ac2d0a479ac39acf403fd5f804atree | snapshot
parentaff6791b3666237a8f95f2eb9d877c1b89b03161commit | 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
components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.