diff options
| author | Pierre-Marie Pédrot | 2016-11-11 18:20:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:43 +0100 |
| commit | 53fe23265daafd47e759e73e8f97361c7fdd331b (patch) | |
| tree | cf22dc2b4477bfe608eea97e73a2c1042b1ea478 /proofs/refine.mli | |
| parent | 7267dfafe9215c35275a39814c8af451961e997c (diff) | |
Refine API using EConstr.
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index 4158e446cc..205b979747 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -21,7 +21,7 @@ val pr_constr : (** {7 Refinement primitives} *) -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** In [refine ?unsafe 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 @@ -30,16 +30,16 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) -val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic (** A generalization of [refine] which assumes exactly one goal under focus *) (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * EConstr.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 : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) |