diff options
| author | jforest | 2007-07-06 19:55:53 +0000 |
|---|---|---|
| committer | jforest | 2007-07-06 19:55:53 +0000 |
| commit | 5168a1b2383c34c40a4ec310ff4e4d990794df2e (patch) | |
| tree | 82d6461b81c4918cf03304dee2e723facc2e42f3 | |
| parent | a91d36f6800bcb341f37211f42774724a6658a2b (diff) | |
minor bug correction (continuing r 9943)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9956 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 213ec18a1c..afbe1c933d 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1237,7 +1237,7 @@ let rec introduce_all_values_eq cont_tac functional termine [cont_tac pmax' le_proofs'; h_intros [heq;heq2]; observe_tac "rewriteRL" (tclTRY (rewriteLR (mkVar heq2))); - tclTHENS + tclTRY (tclTHENS ( fun g -> let t_eq = compute_renamed_type g (mkVar heq) in let k_id,def_id = @@ -1259,7 +1259,7 @@ let rec introduce_all_values_eq cont_tac functional termine [tclIDTAC; tclTHENLIST [apply (delayed_force le_lt_n_Sm); - compute_le_proofs le_proofs']]]) + compute_le_proofs le_proofs']])]) functional termine f p heq1 new_pmax (p'::bounds)((mkVar pmax)::le_proofs) eqs (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] |