correction de bug dans Function et augmentation de la classe des fonctions supportees

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

1 files changed, 33 insertions, 27 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bd4cd0d8c9..be50c4bdbe 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -620,35 +620,41 @@ let build_proof
     : tactic =
   let rec build_proof_aux do_finalize dyn_infos : tactic = 
     fun g -> 
-      
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
 	match kind_of_term dyn_infos.info with 
-	  | Case(_,_,t,_) -> 
-	      let g_nb_prod = nb_prod (pf_concl g) in
-	      let type_of_term = pf_type_of g t in
-	      let term_eq =
-		make_refl_eq type_of_term t
+	  | Case(ci,ct,t,cb) -> 
+	      let do_finalize_t dyn_info' = 
+		fun g ->
+		  let t = dyn_info'.info in 
+		  let dyn_infos = {dyn_info' with info = 
+		      mkCase(ci,ct,t,cb)} in
+		  let g_nb_prod = nb_prod (pf_concl g) in
+		  let type_of_term = pf_type_of g t in
+		  let term_eq =
+		    make_refl_eq type_of_term t
+		  in
+		  tclTHENSEQ
+		    [
+		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      thin dyn_infos.rec_hyps;
+		      pattern_option [[-1],t] None;
+		      h_simplest_case t;
+		      (fun g' -> 
+			 let g'_nb_prod = nb_prod (pf_concl g') in 
+			 let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+			 		     observe_tac "treat_new_case"
+			 (treat_new_case  
+			    ptes_infos
+			    nb_instanciate_partial 
+			    (build_proof do_finalize) 
+			    t 
+			    dyn_infos)
+			   g'
+		      )
+			
+		    ] g
 	      in
-	      tclTHENSEQ
-		[
-		  h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
-		  thin dyn_infos.rec_hyps;
-		  pattern_option [[-1],t] None;
-		  h_simplest_case t;
-		  (fun g' -> 
-		     let g'_nb_prod = nb_prod (pf_concl g') in 
-		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-(* 		     observe_tac "treat_new_case"  *)
-		       (treat_new_case  
-		       ptes_infos
-		       nb_instanciate_partial 
-		       (build_proof do_finalize) 
-		       t 
-		       dyn_infos)
-		       g'
-		  )
-		  
-		] g
+	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
 	      begin
 		match kind_of_term( pf_concl g) with
@@ -752,7 +758,7 @@ let build_proof
 	  | Rel _ -> anomaly "Free var in goal conclusion !" 
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-     (build_proof_aux do_finalize dyn_infos) g
+    observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in