ManTa 3.1 Beta 6 Jul/2001
-------------------------

- Rewriting  strategy  changed  to  innermost (with  this  change  the
  theorem prover benchmark now gives 11% of success --before it gave 10%).
- New  installation scheme that allows  multiple users under Unix.
- Includes a tool to configure manta for final users: manconf.
- Bug fixes (Emacs interface works  with newer versions of emacs, test
  program prp works in DOS withouth long file name support).


ManTa 3.1 Beta 5
----------------

- New sources coverage test and more test cases. Now more than 80%
  of the ManTa kernel is tested and works.
- New procedure to identify memory problems (under Linux).
- Fixes for many memory problems.  Now the test program runs without 
  memory errors !
- The sources require less space, since some unused parts were
  removed
- The translator to ocaml now can be generated and compiled with DJGPP
  in Windows.  (it was not possible before due to memory problems).
- Compiles and runs under DOS without Long File Names.  (Tested with
  DOSEMU running MS-DOS 6.22). However the rewriting motor is not
  working in that platform.


ManTa 3.1 Beta 4
----------------

- New independent tools: mancomp (compiler), manrew (rewriting motor),
  mantheo (theorem prover), m2c (C code generator)
- New ocaml code generator as an independent tool: m2ocaml
- Along with this version the ManTa Benchmark is included.  It is based on
  the NQTHM92 Benchmark.  
- A new rewriting algorithm has been implemented
- Better test programs: They check the rewriting module, the theorem prover,
  the prototype generator, the independent tools and the plain interface.
- More documentation is included with this distribution (formal language 
  description,   technical manual of kernel API, draft of user manual and 
  draft of a tutorial)
- Several bugs have been fixed: 
  - It checks strong local confluence
  - Better unification algorithm
  - Parser can recognize remarks
  - Better typing 
  - When user loads a type it loads all the dependent types
  - Better administration of symbols table
  - Support for longer expressions in ADTs
  - Better memory administration in inductive proofs
- Improvements in the development process
  - New coding and documentation standards
  - Better tools to generate makefiles, documentation and distributions



ManTa 3.1 Beta 3
----------------

- The theory behind ManTa has been revised and the consecuences are:
  . Minor changes in grammar:
      Now an ADT without generators can be defined
      Selectors can have empty domain (and they are used without () )
      A selector can have any domain and any codomain
  . New semantic for restriction, direct sum, completation, variation
  . Representations are ADT and now they work
  . More restrictions to ADT and functions names to avoid conflicts with EQUAL
  . An ADT header now can't have "=string" in:
    ADT name[parameters]=string
- Improvements in selectors definitions:
  . Each axiom has to be left linear
  . Each axiom has to be locally confluent
  . Each selector has to be a total function (Total covering)
- The EMACS interface now works. You can use EMACS 18.* or newer
- Now it evaluates correctly "if" clauses.  (it is not strict)
- Symbols name administration to avoid name conflicts
- Test program to ensure platform independence
- Better memory managment
- Variable numbering in selectors definition fixed
- Bug fixed in Cartesian Product, it generated PROY_p1(N1,N2) and it
  had to be PROY_p1(N1)
- The source code requires less space



ManTa 3.1 Beta 2
----------------

- Platform dependent bugs were fixed
- Asserts added to verify precondition in every function
- Memory allocation and file operations are verified 
- The source code was indented
- Some fixes in creation of new types by direct sum and completion
- Minor fixes in C code generation
- Fix in a function of type NAT (in function DIV)
- Now it allows to edit code generated 



ManTa 3.1 Beta 1
----------------

- New directories hierarchy.  It supports version control and development
  for several platforms
- New names for files, it is apropiate for developing in several platforms
- All the platform dependant functions has been defined in one module that
  is the only module that change from one platform to other.
- New makefiles for each supported platform (gcc in Unix, BC++, Cygnus, Djggp
  in DOS)
- You can find the log of changes in file cam30a31.txt