diff options
| author | jforest | 2006-05-07 00:12:29 +0000 |
|---|---|---|
| committer | jforest | 2006-05-07 00:12:29 +0000 |
| commit | 9b963bd7cacb8eb9c2b923be83f0db67f69d6401 (patch) | |
| tree | b38b4dbc23fb49c500004900f376bce89401f898 /contrib/funind | |
| parent | 6933573c976f68c6275ffd1d9a0598ff2e8aa37f (diff) | |
+ 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
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 12 |
1 files changed, 3 insertions, 9 deletions
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 |