aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r--proofs/goal.mli15
1 files changed, 12 insertions, 3 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli
index c07c7f28e..718d23ccc 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -31,6 +31,10 @@ val pr_goal : goal -> Pp.std_ppcmds
val advance : Evd.evar_map -> goal -> goal option
+(* Equality function on goals. Return [true] if all of its hypotheses
+ and conclusion are equal. *)
+val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
+
(*** Goal tactics ***)
@@ -126,6 +130,9 @@ val rename_hyp : Names.Id.t -> Names.Id.t -> subgoals sensitive
(*** Sensitive primitives ***)
+(* representation of the goal in form of an {!Evd.evar_info} *)
+val info : Evd.evar_info sensitive
+
(* [concl] is the conclusion of the current goal *)
val concl : Term.constr sensitive
@@ -175,6 +182,9 @@ val list_map :
'a list -> Evd.evar_map ->
'b list * Evd.evar_map
+(* emulates List.map for [sensitive] Kleisli functions. *)
+val sensitive_list_map : ('a -> 'b sensitive) -> 'a list -> 'b list sensitive
+
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
internal types. *)
@@ -204,9 +214,6 @@ module V82 : sig
Evd.Store.t ->
goal * Term.constr * Evd.evar_map
- (* Equality function on goals *)
- val equal : Evd.evar_map -> goal -> goal -> bool
-
(* Creates a dummy [goal sigma] for use in auto *)
val dummy_goal : goal Evd.sigma
@@ -238,4 +245,6 @@ module V82 : sig
(* Goal represented as a type, doesn't take into account section variables *)
val abstract_type : Evd.evar_map -> goal -> Term.types
+ val to_sensitive : (goal Evd.sigma -> 'a) -> 'a sensitive
+ val change_evar_map : Evd.evar_map -> unit sensitive
end