diff options
| author | jforest | 2006-08-11 14:36:07 +0000 |
|---|---|---|
| committer | jforest | 2006-08-11 14:36:07 +0000 |
| commit | 6fd0922df95052a7adf68c0fc131bf32365386fb (patch) | |
| tree | f5b7a31b3d5dd412c022aa9df31645c902a325ca /contrib/recdef | |
| parent | 41e4d9cb0757f8057c0815fa0679e888e57ab604 (diff) | |
Bug corrections in Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/recdef')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index d6b0d658c9..93db0eab21 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -287,14 +287,14 @@ let simpl_iter () = onConcl let tclUSER is_mes l g = - let b,l = + let clear_tac = match l with - None -> true,[] - | Some l -> false,l + | None -> h_clear true [] + | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l) in tclTHENSEQ [ - (h_clear b l); + clear_tac; if is_mes then unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] else tclIDTAC @@ -631,7 +631,7 @@ let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_t ) [ (* interactive proof of the well_foundness of the relation *) - wf_tac is_mes (Some args_id); + observe_tac "wf_tac" (wf_tac is_mes (Some args_id)); (* well_foundness -> Acc for any element *) observe_tac "apply wf_thm" |