]> matita.cs.unibo.it Git - helm.git/commit
Many many improvements:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 May 2002 09:17:54 +0000 (09:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 May 2002 09:17:54 +0000 (09:17 +0000)
commitee35bf33520d92753899985329cc4bfee141b808
tree6f0fee9b81ff9ba6a357d8ae1d3ac79b9c37fbf9
parent06e9498bf967323fe12d6383ec7b279a4546a06c
Many many improvements:
1) First version after the introduction of explicit substitutions and
   the change in the DTD and in the stylesheets.
2) ElimIntros (that didn't work) have been replace by ElimIntrosSimpl
   that now does what the name tells you.
3) Buttons to move to the next and previous open goal introduced.
4) Serious bug in reduce and in simpl fixed: they didn't handle the environment
   properly.
5) replace is now an hygher order function, parametrized w.r.t. the equality
   to use. In some cases the right equality is physical equality. This closes
   some residual bugs.
helm/gTopLevel/cic2Xml.ml
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/logicalOperations.ml
helm/gTopLevel/mquery.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/proofEngineReduction.ml
helm/gTopLevel/sequentPp.ml