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.
---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 1f1bdf4da7..9540d3de44 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -677,7 +677,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
+  let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
   let (ev, _) = destEvar sigma ev in
   let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
-- 
cgit v1.2.3