(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * 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 is the recommended way to write tactics when the proof term is easy to write down. Note that this is not the user-level refine tactic defined
in Ltac which is actually based on the one below. *)
open Proofview
(** {6 The refine tactic} *)
(** {7 Refinement primitives} *)
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 [typecheck] is [true] [t] is type-checked beforehand.
Shelved evars and goals are all marked as unresolvable for typeclasses. *)
val refine_with_principal : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t * Evar.t option) -> unit tactic (** Like [refine], but if the [Evar.t option] is [Some ev] then [ev]
inherits properties (the name) of the goal. *)
val generic_refine : typecheck:bool -> ('a * EConstr.t * Evar.t option) tactic ->
Proofview.Goal.t -> 'a tactic (** The general version of refine. *)
(** {7 Unification constraint handling} *)
val solve_constraints : unit tactic (** Solve any remaining unification problems, applying heuristics. *)
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
