- 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

1 files changed, 6 insertions, 0 deletions

diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 5dcdb15c5..4df239e32 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -106,3 +106,9 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
    returns the set of variables appearing in a pattern 
 *)
 val   ids_of_pat : cases_pattern -> Names.Idset.t 
+
+
+(* 
+   removing let_in construction in a rawterm 
+*)
+val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr