diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6dcafb77..5cd703a2 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,15 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Legacy proof engine. Do not use in newly written code. *) open Evd open Proof_type +open EConstr (** The refiner (handles primitive rules and high-level tactics). *) @@ -17,7 +20,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma @@ -30,16 +33,16 @@ val refiner : rule -> tactic (** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic +val tclEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic -val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic +val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic +val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -99,7 +102,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (** A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (** Takes an exception and either raise it at the next level or do nothing. *) @@ -115,13 +118,11 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> Pp.std_ppcmds -> tactic -val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic +val tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic -val tclNOTSAMEGOAL : tactic -> tactic (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, if it succeeds, applies [tac2] to the resulting subgoals, |