- library/list/list.ma: unused code commented
- proceduralClassify type argument are no longer critical: let's see how it goes
- acic2Procedural: the inline parameter Debug now works
- procedural2: we remove the conversions before first order relexivities (exp. to avoid conversion to []=[] in list/list.ma [does not work because []=[] in an open term since the equality type is unspecified]). so we we strengthen reflexivity (see below)
- setoids: now reflexivity is retried after whd if it fails in the first place.
- grafiteAst: detection of convertible rewrites is now optional and activated with the inline parameter "cr". nat/factorial2 is very slow without rewrites
transcript: we now avoid the generation of dupplicated inlines (mistakely generated by the grafite parser [this can not be avoided without a better syntax for .ma scripts])
now list/list.ma is fully reconstructed :)
nat/factorial2.ma takes long to be produced 22m31. Some conversion is slowing the process. nat/bertrand.ma also: we are waiting for it now :(