diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-06 21:34:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-06 21:34:37 +0000 |
| commit | f1967c38371e3d9cd7c38623540e5191c7cd2d6e (patch) | |
| tree | 7110d004c26af9646f582d167a360e82946b3fb9 /tactics/refine.ml | |
| parent | 4ffffb89d777b1a298ca979025625a9149e7e8ac (diff) | |
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
Diffstat (limited to 'tactics/refine.ml')
| -rw-r--r-- | tactics/refine.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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) |