- 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, 25 insertions, 5 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 1173e1a410..14dfbdffce 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -909,6 +909,9 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
       ]
   in
   Command.start_proof
+    (*i The next call to mk_equation_id is valid since we are constructing the lemma
+      Ensures by: obvious
+      i*) 
     (mk_equation_id f_id)
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
@@ -920,16 +923,33 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 
   
 let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
-  let f_id = id_of_label (con_label (destConst f)) in 
-  let equation_lemma_id = (mk_equation_id f_id) in 
   let equation_lemma = 
     try 
-      Tacinterp.constr_of_id (pf_env g) equation_lemma_id 
-    with Not_found -> 
+      let finfos = find_Function_infos (destConst f) in 
+      mkConst (out_some finfos.equation_lemma)
+    with (Not_found | Failure "out_some" as e) -> 
+      let f_id = id_of_label (con_label (destConst f)) in 
+      (*i The next call to mk_equation_id is valid since we will construct the lemma
+	Ensures by: obvious
+	i*) 
+      let equation_lemma_id = (mk_equation_id f_id) in 
       generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+      let _ =
+	match e with 
+	  | Failure "out_some" -> 
+	      let finfos = find_Function_infos (destConst f) in 
+	      update_Function 
+		{finfos with
+		   equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
+					      ConstRef c -> c
+					    | _ -> Util.anomaly "Not a constant" 
+					 )
+		}
+	  | _ -> () 
+
+      in 
       Tacinterp.constr_of_id (pf_env g) equation_lemma_id
   in
-(*   observe (Ppconstr.pr_id equation_lemma_id ++ str " has type " ++ pr_lconstr_env (pf_env g) (pf_type_of g equation_lemma)); *)
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
       (tclDO nb_intro_to_do intro)