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/goal.mli | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

(limited to 'proofs/goal.mli')

diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a79c1f4..dc986315 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.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)         *)
 (************************************************************************)
 
 (** This module implements the abstract interface to goals. Most of the code
@@ -15,12 +17,9 @@ type goal = Evar.t
 (* Gives a unique identifier to each goal. The identifier is
    guaranteed to contain no space. *)
 val uid : goal -> string
-(* Returns the goal (even if it has been partially solved)
-   corresponding to a unique identifier obtained by {!uid}. *)
-val get_by_uid : string -> goal
 
 (* Debugging help *)
-val pr_goal : goal -> Pp.std_ppcmds
+val pr_goal : goal -> Pp.t
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
@@ -38,7 +37,7 @@ module V82 : sig
   val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
   (* Access to ".evar_concl" *)
-  val concl : Evd.evar_map -> goal -> Term.constr
+  val concl : Evd.evar_map -> goal -> EConstr.constr
 
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t
@@ -48,23 +47,20 @@ module V82 : sig
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
-                         Term.constr ->
+                         EConstr.constr ->
                          Evd.Store.t ->
-                         goal * Term.constr * Evd.evar_map
+                         goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
-  (* Principal part of the weak-progress tactical *)
-  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-   
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-    
+
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
@@ -75,6 +71,6 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> Term.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end
-- 
cgit v1.2.3