diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1c7b8d49f..c81e7ce3f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -554,7 +554,7 @@ let subst_var_with_hole occ tid t = else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true)))) + Evar_kinds.QuestionMark(Evar_kinds.Define true), None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -565,13 +565,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)) -> + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),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))) + Evar_kinds.QuestionMark(Evar_kinds.Define true),s)) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 337ae5241..2e3b6e1af 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1511,7 +1511,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) +let cHole = CHole (Loc.ghost, None, None) let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in |