]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7607dbb) | patch
- idtac used for debugging removed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Oct 2002 15:24:56 +0000 (15:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Oct 2002 15:24:56 +0000 (15:24 +0000)
commit1d2bd140d14561951f8214edf15abe4f40dcb649
tree75ade588a34c7e62c975b8db376011bd3d9036d2tree | snapshot
parent7607dbbaf3c411a62300da0594c8b078bca091c5commit | diff
- idtac used for debugging removed
- bug fixed: the natural number 1 was mapped to (Rplus R1 R0).
  It is now mapped to R1 (as it should be). This close all the
  residual bugs.

Still to do: we need to close the last open branch using equality_replace,
as soon as it is implemented.
helm/gTopLevel/fourierR.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.