diff options
| -rw-r--r-- | proofs/proofview.mli | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 234c3fff9..b10cc1843 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -416,8 +416,9 @@ module Goal : sig val refresh_sigma : 'a t -> 'a t tactic end -(** A light interface for building tactics out of partial term. It should be - easier to use than the {!Goal} one. *) +(** A light interface for building tactics out of partial term. Be careful, + the [refine] function does not do any typechecking, so you may construct + ill-typed terms without noticing. *) module Refine : sig type handle @@ -430,9 +431,6 @@ module Refine : sig handle -> Environ.env -> Names.constructor -> handle * Constr.pconstructor (** Creates a constructor with fresh universe variables. *) - val with_type : handle -> Environ.env -> Term.constr -> Term.types -> handle*Term.constr - (** [with_type h env c t] coerces refinable term [c] to type [t]. *) - val update : handle -> (Evd.evar_map -> Evd.evar_map * 'a) -> handle * 'a (** [update h f] update the handle by applying [f] to the underlying evar map. The [f] function must be monotonous, that is, for any evar map [evd], @@ -446,8 +444,8 @@ module Refine : sig function are caught. *) val refine_casted : (handle -> handle * Constr.t) -> unit tactic - (** Like {!refine} except the refined term is coerced to has, as its - type, the conclusion of the current goal. *) + (** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) end |