diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index c772525c86..764a4a0058 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,7 +24,7 @@ type proofview ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) val proofview : proofview -> Evar.t list * Evd.evar_map @@ -95,7 +95,7 @@ type focus_context instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) val focus_context : focus_context -> Evar.t list * Evar.t list @@ -244,15 +244,12 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** [tclFOCUS i j t] applies [t] after focusing on the goals number [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). this - exception is caught at toplevel with a default message + a hook - message that can be customized by [set_nosuchgoals_hook] below. - This hook is used to add a suggestion about bullets when - applicable. *) + existing goals, fails with the [nosuchgoal] argument, by default + raising [NoSuchGoals] (a user error). This exception is caught at + toplevel with a default message. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.t) -> unit -val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSLIST li t] applies [t] on the list of focused goals described by [li]. Each element of [li] is a pair [(i, j)] denoting @@ -261,13 +258,14 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic intervals. If the set of such goals is not a single range, then it will move goals such that it is a single range. (So, for instance, [[1, 3-5]; idtac.] is not the identity.) - If the set of such goals is empty, it will fail. *) -val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + If the set of such goals is empty, it will fail with [nosuchgoal], + by default raising [NoSuchGoals 0]. *) +val tclFOCUSLIST : ?nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its - number.*) -val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + number. Fails with [nosuchgoal], by default raising [NoSuchGoals 1]. *) +val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic (** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the specified range doesn't correspond to existing goals, behaves like @@ -383,7 +381,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Safe_typing.private_constants -> unit tactic +val tclEFFECTS : Evd.side_effects -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic @@ -400,14 +398,23 @@ val give_up : unit tactic val tclPROGRESS : 'a tactic -> 'a tactic module Progress : sig - val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether + the [evar_info] from [evd] corresponding to [evar] is equal to that + from [extended_evd] corresponding to [extended_evar], up to + existential variable instantiation and equalisable universes. The + universe constraints in [extended_evd] are assumed to be an + extension of the universe constraints in [evd]. *) + val goal_equal : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + Evar.t -> + Evar.t -> + bool end (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic -exception Timeout - (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic @@ -507,10 +514,6 @@ module Goal : sig (** Type of goals. *) type t - (** Normalises the argument goal. *) - val normalize : t -> t tactic - [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"] - (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the @@ -601,7 +604,7 @@ module V82 : sig val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evar.t list + val top_evars : entry -> proofview -> Evar.t list (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as |