diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 |
2 files changed, 5 insertions, 4 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 diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 30ee5c514..bd2074139 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1766,7 +1766,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, None) +let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in |