diff options
| author | Pierre-Marie Pédrot | 2015-08-19 19:05:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-08 12:02:50 +0200 |
| commit | dcd0e227295d1250234e027ba11289247de64e37 (patch) | |
| tree | 1b888b5380ecf2f29d19c0af5e5c5d6025b6f545 | |
| parent | 6a246d5d5ec12f618d241407092691595b4f733b (diff) | |
More potentialities in proof_terminators.
| -rw-r--r-- | stm/lemmas.ml | 14 | ||||
| -rw-r--r-- | stm/lemmas.mli | 13 |
2 files changed, 21 insertions, 6 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index af4178eeda..df10e7376a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -351,8 +351,11 @@ let universe_proof_terminator compute_guard hook = let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) -let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = standard_proof_terminator compute_guard hook in +let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> standard_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -361,8 +364,11 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = !start_hook c; Pfedit.start_proof id kind sigma sign c ?init_tac terminator -let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = universe_proof_terminator compute_guard hook in +let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> universe_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 6556aa2297..dca6afe19b 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -24,11 +24,15 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> unit @@ -40,6 +44,11 @@ val start_proof_with_initialization : (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (Proof_global.proof_universes option -> unit declaration_hook) -> + Proof_global.proof_terminator + val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator |