diff options
author | 2010-05-07 09:47:30 +0000 | |
---|---|---|
committer | 2010-05-07 09:47:30 +0000 | |
commit | 4c81b89adf6e93f9686d2a977d09651428a9f99e (patch) | |
tree | 7593f0615c8a6cd070ae59b05178384f8defc3bd | |
parent | b722cd7854c4034f2aae093a545f5aea1141a522 (diff) |
Correction of a bug pointed by P. Casteran.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12998 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | plugins/funind/recdef.ml | 66 |
1 files changed, 23 insertions, 43 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5cf336b65..b5f13270d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -912,12 +912,12 @@ let is_rec_res id = let clear_goals = let rec clear_goal t = match kind_of_term t with - | Prod(Name id as na,t,b) -> + | Prod(Name id as na,t',b) -> let b' = clear_goal b in if noccurn 1 b' && (is_rec_res id) then pop b' else if b' == b then t - else mkProd(na,t,b') + else mkProd(na,t',b') | _ -> map_constr clear_goal t in List.map clear_goal @@ -925,29 +925,14 @@ let clear_goals = let build_new_goal_type () = let sub_gls_types = get_current_subgoals_types () in + (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sub_gls_types in + (* Pp.msgnl (str "sub_gls_types2 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let res = build_and_l sub_gls_types in res - - (* -let prove_with_tcc lemma _ : tactic = - fun gls -> - let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in - tclTHENSEQ - [ - h_generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); - gen_eauto(* default_eauto *) false (false,5) [] (Some []) - (* default_auto *) - ] - gls - *) - - - let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = + (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) let current_proof_name = get_current_proof_name () in let name = match goal_name with | Some s -> s @@ -1033,28 +1018,23 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ by (tclIDTAC) else begin - let _ = msgnl (str "TOTO") in - by (tclIDTAC); - - (* by ( *) - (* fun g -> *) - (* tclTHEN *) - (* (decompose_and_tac) *) - (* (tclORELSE *) - (* (tclFIRST *) - (* (List.map *) - (* (fun c -> *) - (* tclTHENSEQ *) - (* [intros; *) - (* h_simplest_apply (interp_constr Evd.empty (Global.env()) c); *) - (* tclCOMPLETE Auto.default_auto *) - (* ] *) - (* ) *) - (* using_lemmas) *) - (* ) tclIDTAC) *) - (* g); *) - let _ = msgnl (str "TOTO") in - () + by ( + fun g -> + tclTHEN + (decompose_and_tac) + (tclORELSE + (tclFIRST + (List.map + (fun c -> + tclTHENSEQ + [intros; + h_simplest_apply (interp_constr Evd.empty (Global.env()) c); + tclCOMPLETE Auto.default_auto + ] + ) + using_lemmas) + ) tclIDTAC) + g) end; try by tclIDTAC; (* raises UserError _ if the proof is complete *) @@ -1433,7 +1413,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in - let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in + (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in |