diff options
| author | Maxime Dénès | 2019-01-25 17:47:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-05 09:36:51 +0100 |
| commit | 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 (patch) | |
| tree | e6697a39eb0cfb7b45a08e88dd08ad2fe7eedadb /proofs/refine.mli | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
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.
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 11 |
1 files changed, 0 insertions, 11 deletions
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 |