diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 13:31:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 13:31:49 +0000 |
| commit | b31a26f32f2600ba88653086a871dc1fafce4d4d (patch) | |
| tree | 0124d8e846301c5dc43cd4e4700a7da5e2cfcef0 /pretyping/evarutil.mli | |
| parent | a92886745e044266e062651601f60745427bc5a2 (diff) | |
New strategy to infer return predicate of match construct when
external type has evars. We now create a new ad hoc evar instead of
having evars as arguments of evars and use filters to resolved them as
was done since about r10124. In particular, this completes the
resolution of bug 2615.
Evar filters for occurrences might be obsolete as a consequence of
this commit.
Also, abstract_tycon, evar_define, second_order_matching which all
implement some form of second_order_matching should eventually be
merged (abstract_tycon looks for subterms up to delta while
second_order_matching currently looks for syntactic equal subterms,
evar_define doesn't consider the possible dependencies in
non-variables-nor-constructors subterms but has a better handling of
aliases, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14592 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 365276853..54fc07265 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -62,6 +62,16 @@ type conv_fun = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> existential -> constr -> evar_map +val materialize_evar_from_sign : + (env -> evar_map -> existential -> constr -> evar_map) -> + env -> evar_map -> int -> + named_context_val -> bool list -> constr list -> types -> + evar_map * constr * existential + +val solve_evar_evar : + (env -> evar_map -> existential -> constr -> evar_map) -> + env -> evar_map -> existential -> existential -> evar_map + (** {6 Evars/Metas switching...} *) (** [evars_to_metas] generates new metavariables for each non dependent |