]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/proofEngineHelpers.ml
when use_only_paramod is true do not calculate the universe for applicative reasoning
[helm.git] / helm / software / components / tactics / proofEngineHelpers.ml
2006-08-28 Ferruccio Guidi- Level-1: some fixes to the extraction procedure
2006-06-28 Ferruccio Guidi- "linear" flag added to lapply (automatic clearing)
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/