]> matita.cs.unibo.it Git - helm.git/commit
Build_proof_goal does not return the metasenv any more.
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 26 Apr 2006 14:53:03 +0000 (14:53 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 26 Apr 2006 14:53:03 +0000 (14:53 +0000)
commitd5950e1810f3a6d89328f18c2c5796e54a907473
tree974dad13dba0e7165b1ea6818e0362adc53a2f96
parentc6d4fef535f3e4c5e8b8d3c83820e823bb69bbc9
Build_proof_goal does not return the metasenv any more.
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/equality.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/saturation.ml
components/tactics/tactics.mli