From 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 17:47:03 +0100
Subject: Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
---
 tactics/leminv.ml  | 2 +-
 tactics/tactics.ml | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 356b43ec14..48997163de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -250,7 +250,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
 let add_inversion_lemma_exn ~poly na com comsort bool tac =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma, c = Constrintern.interp_type_evars env sigma com in
+  let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
   let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
   try
     add_inversion_lemma ~poly na env sigma c sort bool tac
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5..afa623741a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1155,7 +1155,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;
+}
 
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
-- 
cgit v1.2.3