GitLab

the original file is properly saved and restored upon completion
(whatever the result is)

First working prototype of induction tactic working with lexicographic orders according to type definition

Alt-Ergo still fails at proving the following goal about distributivity though.

theory Test
  use import bool.Bool
  goal G: forall x y z:bool. andb (orb x y) z = orb (andb x z) (andb y z)
end

Update floating_point.GenFloat to new Coq realization format, so as to ease tracking of the original theory.

It cannot be made part of the update-coq Makefile target due to some
peculiarities (sections and records) that are not supported.

- get rid of val_decl, the psymbol/pvsymbol is enough
- get rid of vtv_vars, keep the varset in pvsymbol
- include fresh regions in pd_news (will serve for clone)