diff options
| author | letouzey | 2011-02-03 20:22:33 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-03 20:22:33 +0000 |
| commit | c97a507293db3d4627250ecc433d71f48b0df130 (patch) | |
| tree | 11f39ffdeb879f2a36f69aeee31e9651bf6c94d3 /pretyping/evarutil.mli | |
| parent | 177fd2107c451c477ac839af339c698e10b9df18 (diff) | |
Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)
After r13717, we concentrate on undefined evars. But doing so
too naively was breaking Class_tactics.split_evars, since defined
evars may point to undefined ones. We should not ignore them,
but rather traverse them, which is now done by functions
Evarutil.undefined_evars_of_*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d3a2452de4..38da536834 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -96,10 +96,22 @@ val is_unification_pattern : env * int -> constr -> constr array -> constr -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr +(** The following functions return the set of evars immediately + contained in the object, including defined evars *) + val evars_of_term : constr -> Intset.t val evars_of_named_context : named_context -> Intset.t val evars_of_evar_info : evar_info -> Intset.t +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +val undefined_evars_of_term : evar_map -> constr -> Intset.t +val undefined_evars_of_named_context : evar_map -> named_context -> Intset.t +val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t + (** {6 Value/Type constraints} *) val judge_of_new_Type : unit -> unsafe_judgment |