diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/funind/recdef.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/funind/recdef.ml')
| -rw-r--r-- | contrib/funind/recdef.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 5bd7a6b2..6dc0d5bf 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *) open Term open Termops @@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation (observe_tac "first assert" (assert_tac - true (* the assert thm is in first subgoal *) (Name wf_rec_arg) (mkApp (delayed_force acc_rel, [|input_type;relation;mkVar rec_arg_id|]) @@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation (observe_tac "second assert" (assert_tac - true (Name wf_thm) (mkApp (delayed_force well_founded,[|input_type;relation|])) ) @@ -1157,12 +1155,12 @@ let rec introduce_all_values_eq cont_tac functional termine [] -> let heq2 = next_global_ident_away true heq_id ids in tclTHENLIST - [forward None (dummy_loc,IntroIdentifier heq2) + [pose_proof (Name heq2) (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); unfold_in_hyp [((true,[1]), evaluable_of_global_reference (global_of_constr functional))] - ((all_occurrences_expr, heq2), Tacexpr.InHyp); + ((all_occurrences_expr, heq2), InHyp); tclTHENS (fun gls -> let t_eq = compute_renamed_type gls (mkVar heq2) in |