blob: cfdcde36e0d3ca45fd29e95c09c7b8f1eba13569 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** The primitive refine tactic used to fill the holes in partial proofs. This
is the recommanded 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} *)
(** Printer used to print the constr which refine refines. *)
val pr_constr :
(Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
(** {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. *)
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 ->
[ `NF ] 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
(** Solve any remaining unification problems, applying heuristics. *)
|
