From b37cc1ad85d2d1ac14abcd896f2939e871705f98 Mon Sep 17 00:00:00 2001 From: jforest Date: Mon, 2 Jun 2008 09:14:23 +0000 Subject: Minor bug correction in recdef git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11036 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/recdef.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 49c07ff72e..f4f852d364 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 ) -- cgit v1.2.3