diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d3f6845c..2b326fd1 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,21 +119,19 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr val evars_of_term : constr -> Intset.t -(** returns the evars contained in the term associated with - the evars they contain themselves in their body, if any. - If the evar has no body, [None] is associated to it. *) -val evars_of_evars_of_term : evar_map -> constr -> (Intset.t option) Intmap.t val evars_of_named_context : named_context -> Intset.t val evars_of_evar_info : evar_info -> Intset.t -(** returns the evars which can be found in the typing context of the argument evars, - in the same format as {!evars_of_evars_of_term}. - It explores recursively the evars in the body of the argument evars -- but does - not return them. *) -(* spiwack: tongue in cheek: it should have been called - [evars_of_evars_in_types_of_list_and_recursively_in_bodies] *) -val evars_of_evars_in_types_of_list : evar_map -> evar list -> (Intset.t option) Intmap.t - +(** [gather_dependent_evars evm seeds] classifies the evars in [evm] + as dependent_evars and goals (these may overlap). A goal is an + evar in [seeds] or an evar appearing in the (partial) definition + of a goal. A dependent evar is an evar appearing in the type + (hypotheses and conclusion) of a goal, or in the type or (partial) + definition of a dependent evar. The value return is a map + associating to each dependent evar [None] if it has no (partial) + definition or [Some s] if [s] is the list of evars appearing in + its (partial) definition. *) +val gather_dependent_evars : evar_map -> evar list -> (Intset.t option) Intmap.t (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. |