Put "ssreflect" behind "API".

2 files changed, 25 insertions, 2 deletions

diff --git a/API/API.mli b/API/API.mli
index 2661badc5e..d844e8bf52 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -809,6 +809,7 @@ sig
   val mkNamedLambda : Names.Id.t -> types -> constr -> constr
   val mkNamedProd : Names.Id.t -> types -> types -> types
 
+  val isCast : Evd.evar_map -> t -> bool
   val isEvar : Prelude.evar_map -> constr -> bool
   val isInd  : Prelude.evar_map -> constr -> bool
   val isRel : Prelude.evar_map -> constr -> bool
@@ -827,6 +828,7 @@ sig
   val destConst : Prelude.evar_map -> constr -> Names.Constant.t * EInstance.t
   val destConstruct : Prelude.evar_map -> constr -> Names.constructor * EInstance.t
   val destFix : Evd.evar_map -> t -> (t, t) Term.pfixpoint
+  val destCast : Evd.evar_map -> t -> t * Term.cast_kind * t
 
   val mkConstruct : Names.constructor -> constr
 
@@ -866,6 +868,8 @@ sig
     val substl : constr list -> constr -> constr
     val lift : int -> constr -> constr
     val liftn : int -> int -> t -> t
+    val subst_var : Names.Id.t -> t -> t
+    val subst_vars : Names.Id.t list -> t -> t
   end
 
   val fresh_global :
@@ -907,6 +911,7 @@ val of_named_decl : (Term.constr, Term.types) Context.Named.Declaration.pt -> (c
   val mkConstU : Names.Constant.t * EInstance.t -> t
   val isProd : Evd.evar_map -> t -> bool
   val mkConstructUi : (Names.inductive * EInstance.t) * int -> t
+  val isLambda : Evd.evar_map -> t -> bool
 end
 
 module Mod_subst :
@@ -3262,10 +3267,11 @@ end
 module Proof_type :
 sig
   type goal = Evar.t
+  type rule = Proof_type.prim_rule =
+    | Cut of bool * bool * Names.Id.t * Term.types
+    | Refine of Term.constr
 
   type tactic = goal Evd.sigma -> goal list Evd.sigma
-
-  type rule = Proof_type.rule
 end
 
 module Redexpr :
@@ -3333,6 +3339,8 @@ sig
 
   val pf_nth_hyp_id : Proof_type.goal sigma -> int -> Names.Id.t
 
+  val sig_it : 'a sigma -> 'a
+
   module New :
   sig
     val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
@@ -3467,6 +3475,11 @@ sig
   val tclREPEAT : Proof_type.tactic -> Proof_type.tactic
   val tclORELSE        : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
   val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic
+  val tclIDTAC : Proof_type.tactic
+  val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+  val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
+  val tclTRY : Proof_type.tactic -> Proof_type.tactic
+  val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
 end
 
 module Termops :
@@ -4031,9 +4044,13 @@ sig
   val cache_term_by_tactic_then :
     opaque:bool -> ?goal_type:(EConstr.constr option) -> Names.Id.t ->
     Decl_kinds.goal_kind -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+  val apply_type : EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
+  val hnf_in_concl : unit Proofview.tactic
+  val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
 
   module New :
   sig
+    val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
     val reduce_after_refine : unit Proofview.tactic
   end
   module Simple :
@@ -4061,7 +4078,12 @@ sig
   val tclTHENS : tactic -> tactic list -> tactic
   val tclFIRST         : tactic list -> tactic
   val tclTHENFIRST     : tactic -> tactic -> tactic
+  val tclTHENLAST      : tactic -> tactic -> tactic
+  val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
+  val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
+  val tclSOLVE         : tactic list -> tactic
 
+  val onClause   : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
   val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
   val onLastHypId : (Names.Id.t -> tactic) -> tactic
   val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 350457f6c2..44aae771f6 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -177,6 +177,7 @@ sig
   val parse_string : 'a Gram.Entry.e -> string -> 'a
   val (!@) : Ploc.t -> Loc.t
   val set_command_entry : API.Vernacexpr.vernac_expr Gram.Entry.e -> unit
+  val to_coqloc : Ploc.t -> Loc.t
 end
 
 module CLexer :