diff options
| author | jforest | 2007-11-26 20:19:02 +0000 |
|---|---|---|
| committer | jforest | 2007-11-26 20:19:02 +0000 |
| commit | 37e86a68a1fface68b9eb05b9304b44e89ba8c06 (patch) | |
| tree | 07e5a733e694a618e57b7de23aa364a2b5a87ef1 | |
| parent | d13613ca7e9a986b94c39b1226619e254f7def29 (diff) | |
minor bug correction in Function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10338 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 20 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 2 |
2 files changed, 16 insertions, 6 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 17a37ec755..b10aa782c8 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1358,8 +1358,17 @@ let rec rewrite_eqs_in_eqs eqs = match eqs with | [] -> tclIDTAC | eq::eqs -> + tclTHEN - (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq) false)) eqs) + (tclMAP + (fun id gl -> + observe_tac + (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) + (tclTRY (Equality.general_rewrite_in true id (mkVar eq) false)) + gl + ) + eqs + ) (rewrite_eqs_in_eqs eqs) let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = @@ -1384,7 +1393,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = observe_tac "rew_and_finish" (tclTHENLIST [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); - rewrite_eqs_in_eqs eqs; + observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); (observe_tac "finishing" (tclCOMPLETE ( Eauto.gen_eauto false (false,5) [] (Some [])) @@ -1595,12 +1604,13 @@ let prove_principle_for_gen (* observe_tac "new_prove_with_tcc" *) (new_prove_with_tcc is_mes acc_inv fix_id - !tcc_list - ((List.map + + (!tcc_list@(List.map (fun (na,_,_) -> (Nameops.out_name na)) (princ_info.args@princ_info.params) - )@ (acc_rec_arg_id::eqs)) + )@ ([acc_rec_arg_id])) eqs ) + ); is_valid = is_valid_hypothesis predicates_names } diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 8dc0705988..a948dd4d64 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -199,7 +199,7 @@ let rec (find_call_occs : int -> constr -> constr -> | Var(id) -> (fun l -> expr), [] | Meta(_) -> error "find_call_occs : Meta" | Evar(_) -> error "find_call_occs : Evar" - | Sort(_) -> error "find_call_occs : Sort" + | Sort(_) -> (fun l -> expr), [] | Cast(b,_,_) -> find_call_occs nb_lam f b | Prod(_,_,_) -> error "find_call_occs : Prod" | Lambda(na,t,b) -> |