From 9b963bd7cacb8eb9c2b923be83f0db67f69d6401 Mon Sep 17 00:00:00 2001 From: jforest Date: Sun, 7 May 2006 00:12:29 +0000 Subject: + correcting a bug in general recursive function (match e with _ => match f e with .... end end was not correctly treated) + cleaning dead code in functional_principles_proofs.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8797 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/functional_principles_proofs.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'contrib/funind') diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 0ee8a7e759..a8ecdfd0e6 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -48,12 +48,6 @@ let observe_tac s tac g = then do_observe_tac (str s) tac g else tac g -(* let observe_stream_tac s tac g = *) -(* if do_observe () *) -(* then do_observe_tac s tac g *) -(* else tac g *) - - let tclTRYD tac = if !Options.debug || do_observe () @@ -1036,8 +1030,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in let id_as_induction_constr = Tacexpr.ElimOnConstr id in (tclTHENSEQ - [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) - Tactics.intros_reflexivity + [new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) + intros_reflexivity ]) ] in @@ -1222,7 +1216,7 @@ let prove_principle_for_gen fun g -> let type_of_goal = pf_concl g in let goal_ids = pf_ids_of_hyps g in - let goal_elim_infos = Tactics.compute_elim_sig type_of_goal in + let goal_elim_infos = compute_elim_sig type_of_goal in let params_names,ids = List.fold_left (fun (params_names,avoid) (na,_,_) -> let new_id = fresh_id avoid na in -- cgit v1.2.3