]> matita.cs.unibo.it Git - helm.git/commit
Generation of inductive principle for Type[0].
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jul 2009 08:58:18 +0000 (08:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jul 2009 08:58:18 +0000 (08:58 +0000)
commitc515405206bfeb9f99d3e175b7f1e390ba299f28
tree2bd03733d8c28205c4912c66dc4e56d379386dc9
parenta687cf5e3e9ae6fb6ead058c4a191002f21fa951
Generation of inductive principle for Type[0].

The way the code has been branched is very messy: we generate an AST and
from it a new command NObj that is recursively processed in GrafiteEngine.
However, disambiguation needs the alias. Thus the aliases for the inductive
principle are immediately generated and added while the others are delayed.
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/ng_tactics/nCicElim.ml
helm/software/components/ng_tactics/nCicElim.mli