From 14cb3c26e5b35a4d824838c76a7cf8d8a0fa35e0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Feb 2019 20:59:01 +0100
Subject: Adapt to https://github.com/coq/coq/pull/9410

---
 src/tac2core.ml    | 6 ++++--
 src/tac2tactics.ml | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 8e92e154ac..b5ae446ed5 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -954,7 +954,8 @@ let constr_flags () =
     use_typeclasses = true;
     solve_unification_constraints = true;
     fail_evar = true;
-    expand_evars = true
+    expand_evars = true;
+    program_mode = false;
   }
 
 let open_constr_no_classes_flags () =
@@ -963,7 +964,8 @@ let open_constr_no_classes_flags () =
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true
+  expand_evars = true;
+  program_mode = false;
   }
 
 (** Embed all Ltac2 data into Values *)
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index b06427bc38..bc92ab43a8 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -22,7 +22,9 @@ let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
   Pretyping.fail_evar = not with_evar;
-  Pretyping.expand_evars = true }
+  Pretyping.expand_evars = true;
+  Pretyping.program_mode = false;
+}
 
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =
-- 
cgit v1.2.3