diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 09:14:23 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 09:14:23 +0000 |
| commit | b37cc1ad85d2d1ac14abcd896f2939e871705f98 (patch) | |
| tree | b5a2b66b4850157ae0c30dae2cb4c713f78a972d | |
| parent | c076bdf8b80da7de215b26934cc6e9a8d0916837 (diff) | |
Minor bug correction in recdef
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11036 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/funind/recdef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 49c07ff72..f4f852d36 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -623,8 +623,8 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn ) -let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = - match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with +let rec_leaf_terminate f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = + match find_call_occs 0 f_constr expr with | context_fn, args -> observe_tac "introduce_all_values" (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) @@ -839,7 +839,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a (mkVar f_id) func base_leaf_terminate - (rec_leaf_terminate concl_tac) + (rec_leaf_terminate (mkVar f_id) concl_tac) [] expr ) |