diff options
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 31 |
1 files changed, 18 insertions, 13 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index a44632ef..70a23a9f 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** The primitive refine tactic used to fill the holes in partial proofs. This @@ -17,30 +19,33 @@ open Proofview (** Printer used to print the constr which refine refines. *) val pr_constr : - (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t (** {7 Refinement primitives} *) -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine ?unsafe t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is - type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic -(** A generalization of [refine] which assumes exactly one goal under focus *) +val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic +(** A variant of [refine] which assumes exactly one goal under focus *) + +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 -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr + 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 : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +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. *) |