From f1967c38371e3d9cd7c38623540e5191c7cd2d6e Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 6 Jun 2009 21:34:37 +0000 Subject: Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 instead of the index required by the user; extended FixRule and Cofix accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/refine.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'tactics/refine.ml') diff --git a/tactics/refine.ml b/tactics/refine.ml index 46c8d3aa2..f1ecc4da9 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -330,29 +330,30 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = gl (* fix => tactique Fix *) - | Fix ((ni,_),(fi,ai,_)) , _ -> + | Fix ((ni,j),(fi,ai,_)) , _ -> let out_name = function | Name id -> id | _ -> error "Recursive functions must have names." in let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in + let firsts,lasts = list_chop j (Array.to_list fixes) in tclTHENS - (mutual_fix (out_name fi.(0)) (succ ni.(0)) - (List.tl (Array.to_list fixes))) + (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j) (List.map (function | None -> tclIDTAC | Some th -> tcc_aux subst th) sgp) gl (* cofix => tactique CoFix *) - | CoFix (_,(fi,ai,_)) , _ -> + | CoFix (j,(fi,ai,_)) , _ -> let out_name = function | Name id -> id | _ -> error "Recursive functions must have names." in let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in + let firsts,lasts = list_chop j (Array.to_list cofixes) in tclTHENS - (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes))) + (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j) (List.map (function | None -> tclIDTAC | Some th -> tcc_aux subst th) sgp) -- cgit v1.2.3