aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/extratactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
-rw-r--r--plugins/ltac/extratactics.ml48
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc43930e4..9d50b6e6f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -631,14 +631,14 @@ let subst_var_with_hole occ tid t =
let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec = function
- | (_, GVar id) as x ->
+ | { CAst.v = GVar id } as x ->
if Id.equal id tid
then
(decr occref;
if Int.equal !occref 0 then x
else
(incr locref;
- Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+ CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
Misctypes.IntroAnonymous, None)))
else x
@@ -651,12 +651,12 @@ 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),Misctypes.IntroAnonymous,s) ->
+ | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
- Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+ CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
| c -> map_glob_constr_left_to_right substrec c
in