From 83afcfd21be0084b2eff33ffd9e2d8b785679d4a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 17 Jul 2018 01:14:36 +0200
Subject: change into QuestionMark default

---
 tactics/hipattern.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 9d2288346..7da059ae3 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -264,9 +264,7 @@ 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 {
-      Evar_kinds.qm_obligation=Define false;
-      Evar_kinds.qm_name=Anonymous;
-      Evar_kinds.qm_record_field=None
+        Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false;
   }, Namegen.IntroAnonymous, None)
 let mkGProd id c1 c2 = DAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
-- 
cgit v1.2.3