diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-15 11:30:08 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-15 11:30:08 +0000 |
| commit | 761a0e31fb463a8d607f445c572d56bb71c22904 (patch) | |
| tree | d9a4cf6f4f75e309cca2abdb741d0befeea810f6 /contrib | |
| parent | 05a07b454b7b1d99950178e19ad2feaa12c44991 (diff) | |
Minor bug correction in well-founded Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9143 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index d780bc1c6..5f2ba1578 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -300,7 +300,14 @@ let rec mk_intros_and_continue (extra_eqn:bool) tclMAP (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq)) (List.rev eqs); - cont_function (mkVar teq::eqs) expr + (fun g1 -> + let ty_teq = pf_type_of g1 (mkVar teq) in + let teq_lhs,teq_rhs = + let _,args = destApp ty_teq in + args.(1),args.(2) + in + cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1 + ) ] g else |