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.

4 files changed, 4 insertions, 33 deletions

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
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6c4193c66b..1b2756f49f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -53,7 +53,9 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.use_typeclasses = true;
       Pretyping.solve_unification_constraints = true;
       Pretyping.fail_evar = false;
-      Pretyping.expand_evars = true } in
+      Pretyping.expand_evars = true;
+      Pretyping.program_mode = false;
+    } in
     try Pretyping.understand_ltac flags
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1d796fece5..06e6b89df1 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -137,26 +137,6 @@ let refine ~typecheck f =
   in
   Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
-(** Useful definitions *)
-
-let with_type env evd c t =
-  let my_type = Retyping.get_type_of env evd c in
-  let j = Environ.make_judge c my_type in
-  let (evd,j') =
-    Coercion.inh_conv_coerce_to true env evd j t
-  in
-  evd , j'.Environ.uj_val
-
-let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
-  let concl = Proofview.Goal.concl gl in
-  let env = Proofview.Goal.env gl in
-  let f h =
-    let (h, c) = f h in
-    with_type env h c concl
-  in
-  refine ~typecheck f
-end
-
 (** {7 solve_constraints}
 
   Ensure no remaining unification problems are left. Run at every "." by default. *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1af6463a02..55dafe521f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -34,17 +34,6 @@ val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
-(** {7 Helper functions} *)
-
-val with_type : Environ.env -> Evd.evar_map ->
-  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
-(** [with_type env sigma c t] ensures that [c] is of type [t]
-    inserting a coercion if needed. *)
-
-val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
-(** Like {!refine} except the refined term is coerced to the conclusion of the
-    current goal. *)
-
 (** {7 Unification constraint handling} *)
 
 val solve_constraints : unit tactic