aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/hipattern.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index f9c4bed35..9d2288346 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,11 @@ open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
let mkGApp f args = DAst.make @@ GApp (f, args)
let mkGHole = DAst.make @@
- GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None)
+ GHole (QuestionMark {
+ Evar_kinds.qm_obligation=Define false;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None
+ }, Namegen.IntroAnonymous, None)
let mkGProd id c1 c2 = DAst.make @@
GProd (Name (Id.of_string id), Explicit, c1, c2)
let mkGArrow c1 c2 = DAst.make @@