From f34f1330b6cce198fdf6f99a31ae46e1a7fa8abb Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 28 Nov 2008 19:40:51 +0000 Subject: another bug with simpl git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/tacred.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index cc5f44c83..d1afdfc2c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -346,7 +346,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) -let substl_with_arity subst c = +let substl_with_arity subst constr = let v = Array.of_list subst in let rec subst_total k c = let (h,rcargs) = decompose_app c in @@ -361,14 +361,14 @@ let substl_with_arity subst c = else mkRel (i - Array.length v) in applist(h',List.map(subst_total k)rcargs) | _ -> map_constr_with_binders succ subst_total k c in - subst_total 0 c + subst_total 0 constr let contract_fix_use_function f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = list_tabulate make_Fi nbodies in - substl_with_arity (List.rev lbodies) bodies.(bodynum) + substl_with_arity (List.rev lbodies) (nf_beta bodies.(bodynum)) let reduce_fix_use_function f whfun fix stack = match fix_recarg fix stack with -- cgit v1.2.3