diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 78a1f51b7..9a9ef164e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -540,12 +540,12 @@ let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function - | RVar (_,id) as x -> + | GVar (_,id) as x -> if id = tid then (decr occref; if !occref = 0 then x - else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) + else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) else x - | c -> map_rawconstr_left_to_right substrec c in + | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t in if !occref > 0 then Termops.error_invalid_occurrence [occ] else t' @@ -554,10 +554,10 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | RHole (_,Evd.QuestionMark(Evd.Define true)) -> + | GHole (_,Evd.QuestionMark(Evd.Define true)) -> decr occref; if !occref = 0 then tc - else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) - | c -> map_rawconstr_left_to_right substrec c + else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) + | c -> map_glob_constr_left_to_right substrec c in substrec t |