]> matita.cs.unibo.it Git - helm.git/commit
lazy proof term to increase sharing and decrease memory consumption.
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 26 Sep 2008 08:03:47 +0000 (08:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 26 Sep 2008 08:03:47 +0000 (08:03 +0000)
commit45a9e84c12f57e5473eccc6f611cdbb343998d5d
treed227a9f407279474fe69d026413665c273392175
parent99feea74c16b4801a2b1596d5e48e27224ffbfaa
lazy proof term to increase sharing and decrease memory consumption.
I hope nobody was comparing grafite-statuses with ocaml polymorphic =
15 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/inversion_principle.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineTypes.ml
helm/software/components/tactics/proofEngineTypes.mli
helm/software/components/tactics/statefulProofEngine.mli
helm/software/matita/matita.ml
helm/software/matita/matitaAutoGui.ml
helm/software/matita/matitaAutoGui.mli
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml