Fixing two minor bugs in recdef and graph of function generation.

Fixing .depend (forgot to remove new_arg_principles dependencies in last commit
) 


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

3 files changed, 21 insertions, 48 deletions

diff --git a/.depend b/.depend
index 7e791bd290..8bd125ae99 100644
--- a/.depend
+++ b/.depend
@@ -432,8 +432,6 @@ contrib/funind/functional_principles_types.cmi: kernel/term.cmi \
     proofs/tacmach.cmi pretyping/rawterm.cmi kernel/names.cmi 
 contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \
     lib/pp.cmi kernel/names.cmi library/libnames.cmi 
-contrib/funind/new_arg_principle.cmi: kernel/term.cmi proofs/tacmach.cmi \
-    pretyping/rawterm.cmi kernel/names.cmi 
 contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \
     kernel/names.cmi library/libnames.cmi 
 contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \
@@ -2966,38 +2964,6 @@ contrib/funind/invfun.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
     library/libnames.cmx pretyping/indrec.cmx \
     contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \
     tactics/extratactics.cmx tactics/equality.cmx kernel/declarations.cmx 
-contrib/funind/new_arg_principle.cmo: toplevel/vernacexpr.cmo \
-    toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \
-    pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tactic_debug.cmi pretyping/tacred.cmi \
-    proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    lib/system.cmi kernel/sign.cmi pretyping/reductionops.cmi \
-    pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
-    pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \
-    lib/options.cmi kernel/names.cmi library/libnames.cmi library/lib.cmi \
-    pretyping/indrec.cmi contrib/funind/indfun_common.cmi \
-    tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \
-    pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \
-    kernel/entries.cmi library/declare.cmi kernel/declarations.cmi \
-    library/decl_kinds.cmo interp/coqlib.cmi toplevel/command.cmi \
-    kernel/closure.cmi toplevel/cerrors.cmi \
-    contrib/funind/new_arg_principle.cmi 
-contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
-    toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \
-    pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tactic_debug.cmx pretyping/tacred.cmx \
-    proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    lib/system.cmx kernel/sign.cmx pretyping/reductionops.cmx \
-    pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
-    pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \
-    lib/options.cmx kernel/names.cmx library/libnames.cmx library/lib.cmx \
-    pretyping/indrec.cmx contrib/funind/indfun_common.cmx \
-    tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \
-    pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \
-    kernel/entries.cmx library/declare.cmx kernel/declarations.cmx \
-    library/decl_kinds.cmx interp/coqlib.cmx toplevel/command.cmx \
-    kernel/closure.cmx toplevel/cerrors.cmx \
-    contrib/funind/new_arg_principle.cmi 
 contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
     tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
     parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index e52688dc0c..b0c4f4cda7 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -564,7 +564,7 @@ and build_entry_lc_from_case funname make_discr
 	in
 	let results =
 	  List.map 
-	    (build_entry_lc_from_case_term funname make_discr []  brl case_resl.to_avoid) 
+	    (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) []  brl case_resl.to_avoid) 
 	    case_resl.result 
 	in 
 	{ 
@@ -639,7 +639,7 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 			       List.for_all (fun x -> x) unif) patterns_to_prevent
 	     then 
 	       let i = List.length patterns_to_prevent in 
-	       [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i  )]
+	       [(Prod Anonymous,make_discr  i  )]
 	     else 
 	       []
 	    )
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index ab0c0f9a50..c232a87a57 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -46,6 +46,9 @@ open Eauto
 open Genarg
 
 
+let qed () = Command.save_named true 
+let defined () = Command.save_named false
+
 let h_intros l = 
   tclMAP h_intro l
 
@@ -61,7 +64,6 @@ let do_observe_tac s tac g =
 let observe_tac s tac g = 
   tac g
 
-
 let hyp_ids = List.map id_of_string
     ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
      "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];;
@@ -371,16 +373,21 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
 	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
 	   tclTHENS
 	     (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
-	     [tclTHENLIST[h_intro h';
-			  simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
-			  default_full_auto]; tclIDTAC];
+	     [
+	       tclTHENLIST[h_intro h';
+			   simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
+			   default_full_auto];
+	       tclIDTAC
+	     ];
 	   observe_tac "clearing k " (clear [k]);
-	   h_intros [k;h';def];
-	   simpl_iter();
-	   unfold_in_concl[([1],evaluable_of_global_reference func)];
-	   list_rewrite true eqs;
-           list_cond_rewrite  k def bound cond_eqs le_proofs;
-	   apply (delayed_force refl_equal)] g
+	   observe_tac "intros k h' def" (h_intros [k;h';def]);
+	   observe_tac "simple_iter" (simpl_iter());
+	   observe_tac "unfold functionnal" 
+	     (unfold_in_concl[([1],evaluable_of_global_reference func)]);
+	   observe_tac "rewriting equations" 
+	     (list_rewrite true eqs);
+           observe_tac "cond rewrite" (list_cond_rewrite  k def bound cond_eqs le_proofs);
+	   observe_tac "refl equal" (apply (delayed_force refl_equal))] g
   | spec1::specs ->
       fun g ->
 	let ids = ids_of_named_context (pf_hyps g) in
@@ -758,7 +765,7 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   =
     let lemma = mkConst (Lib.make_con na) in 
     Array.iteri (fun i _ -> by (observe_tac "tac" (prove_with_tcc lemma i))) (Array.make nb_goal ());
     ref := Some lemma ;
-    Command.save_named true;
+    defined ();
   in
   start_proof
     na
@@ -1029,7 +1036,7 @@ let (com_eqn : identifier ->
 	       )
 	  )
        );
-     Command.save_named true);;
+     defined ());;
 
 
 let recursive_definition is_mes function_name type_of_f r rec_arg_num eq