diff options
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 32 |
1 files changed, 14 insertions, 18 deletions
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 |