diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 34f5b52eb..cb15bb94c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -596,7 +596,8 @@ let subst_var_with_hole occ tid t = else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true), None))) + Evar_kinds.QuestionMark(Evar_kinds.Define true), + Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -607,13 +608,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) -> + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true),s)) + Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t |