]> matita.cs.unibo.it Git - helm.git/commit
- library/list/list.ma: unused code commented
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 10 Jun 2009 20:19:42 +0000 (20:19 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 10 Jun 2009 20:19:42 +0000 (20:19 +0000)
commit82baf094141d9ef518d681b8cebcc180bca14d2c
tree972911afee68ae442302895c954d8fb6b20665bb
parent96c91e470f670018df67c9cbff62fa06e3b57c5e
- 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 :(
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/procedural2.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/binaries/transcript/engine.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/.depend
helm/software/components/tactics/.depend.opt
helm/software/components/tactics/setoids.ml
helm/software/matita/library/list/list.ma