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.
---
 plugins/ssr/ssrcommon.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c3b9bde9b8..0961edb6cb 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -243,7 +243,9 @@ let interp_refine ist gl rc =
     Pretyping.use_typeclasses = true;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true }
+    expand_evars = true;
+    program_mode = false;
+  }
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
-- 
cgit v1.2.3