diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-16 15:09:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-16 15:09:07 +0000 |
| commit | 6c21af13a66a8fd829979476205e32df9e8c0f49 (patch) | |
| tree | 9f3634f39cbeeefff29877db39a353b63c598bc5 /pretyping/evarutil.mli | |
| parent | ec60cad947dc4267f0545626b4ec7145f19f3ee3 (diff) | |
Introducing a notion of evar candidates to be used when an evar is
known in advance to be instantiable by only a finite number of terms.
When an evar with candidates remain unsolved after unification, the
first candidate is taken as a heuristic.
This is used in particular to reduce the number of pending conversion
problems when trying to infer the return clause of a pattern-matching
problem. As an example, this repairs test 2615.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 78898aaa7..61f503c7d 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -28,11 +28,13 @@ val new_untyped_evar : unit -> existential_key (** {6 Creating a fresh evar given their type and context} *) val new_evar : - evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr + evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + ?candidates:constr list -> types -> evar_map * constr (** the same with side-effects *) val e_new_evar : - evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr + evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + ?candidates:constr list -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) @@ -46,7 +48,7 @@ val new_type_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list @@ -219,7 +221,7 @@ val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> identifier list -> named_context_val * types val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list + named_context_val * types * constr list * constr list val generalize_evar_over_rels : evar_map -> existential -> types * constr list |