Imported Upstream version 8.5~beta1+dfsg

1 files changed, 10 insertions, 44 deletions

diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5db43eaf..a81555ff 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,17 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open Sign
+open Context
 open Evd
 open Proof_type
-open Tacexpr
-open Logic
 
 (** The refiner (handles primitive rules and high-level tactics). *)
 
@@ -26,31 +23,22 @@ val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
 
-(** {6 Hiding the implementation of tactics. } *)
-
-(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under
-   a single proof node. The boolean tells if the default tactic is used. *)
-(* spiwack: currently here for compatibility, abstract_operation 
-    is a second projection *)
-val abstract_operation : compound_rule -> tactic -> tactic
-val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
-val abstract_extended_tactic :
-  ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
-
 val refiner : rule -> tactic
 
 (** {6 Tacticals. } *)
 
-(** [tclNORMEVAR] forces propagation of evar constraints *)
-val tclNORMEVAR       : tactic
-
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
+val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+
+val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
+val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+
+val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
@@ -83,10 +71,6 @@ val tclTHENSV         : tactic -> tactic array -> tactic
 (** Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(** [tclTHENST] is renamed [tclTHENSFIRSTn]
-val tclTHENST        : tactic -> tactic array -> tactic -> tactic
-*)
-
 (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
@@ -118,7 +102,7 @@ exception FailError of int * Pp.std_ppcmds Lazy.t
 
 (** Takes an exception and either raise it at the next
    level or do nothing. *)
-val catch_failerror  : exn -> unit
+val catch_failerror  : Exninfo.iexn -> unit
 
 val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
@@ -133,9 +117,9 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclTIMEOUT       : 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,
@@ -150,21 +134,3 @@ val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
    Equivalent to [(tac1;try tac2)||tac2] *)
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
-
-(** {6 Tactics handling a list of goals. } *)
-
-type tactic_list = goal list sigma -> goal list sigma
-
-val tclFIRSTLIST       : tactic_list list -> tactic_list
-val tclIDTAC_list      : tactic_list
-val first_goal         : 'a list sigma -> 'a sigma
-val apply_tac_list     : tactic -> tactic_list
-val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
-val tactic_list_tactic : tactic_list -> tactic
-val goal_goal_list     : 'a sigma -> 'a list sigma
-
-(** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
-   may have unresolved holes; if [solve_holes] these holes must be
-   resolved after application of the tactic; [sigma] must be an
-   extension of the sigma of the goal *)
-val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic