From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 proofs/refine.mli | 31 ++++++++++++++++++-------------
 1 file changed, 18 insertions(+), 13 deletions(-)

(limited to 'proofs/refine.mli')

diff --git a/proofs/refine.mli b/proofs/refine.mli
index a44632ef..70a23a9f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
 (** The primitive refine tactic used to fill the holes in partial proofs. This
@@ -17,30 +19,33 @@ open Proofview
 
 (** Printer used to print the constr which refine refines. *)
 val pr_constr :
-  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+  (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (default is [true]) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
+  Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
 
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * Term.constr
+  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
 
-- 
cgit v1.2.3