- completely new version of "functional inversion" using inversion on

  inductive  

- bug  correction in  "Functional  scheme" and  "functional inversion": the
  function are now parsed as references and not indent

- adding a zeta normalization function in rawtermops to zeta normalize
  graph constructions (not used for now)

- Bug correction  in generation of  functional principle types  (if an
  arguments of the function has a type which is a sort)
  
- adding a new persistent table for functional induction informations
  (graph,...)  

- new  save mechanism  for functional  induction principles  (reuse of
  proofs when possible)

- Minor bug correction in proof of principle.

- Distinguishing building_principles (that is  save them) and making then
  (just construct their proof term)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions