diff options
| author | herbelin | 2011-10-10 22:00:26 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-10 22:00:26 +0000 |
| commit | bfc6434ee257e9e9830f54546ffbd6f4b66e96d4 (patch) | |
| tree | 0521253f4b55c3d5cc6a75b8b6099cd2c02dc9fa /pretyping/evarutil.mli | |
| parent | 698c79dc28a13baf864c863800a2b48690207e34 (diff) | |
More robust and uniform treatment of aliases in evarutil.ml
- Compute chain of aliases once for all so as to simplify code.
- In is_unification_pattern, expand all vars/rels of the unification
problem until they are no longer vars/rels so that the list of
vars/rels used in the rhs is correct, and, the list of arguments of
the evars eventually become irreducible vars/rels (in particular,
this solves bug #2615).
- Some points remain unclear, e.g. whether solve_evar_evar should
reason with all let-in expanded or with let-in expanded only up
to the last expansion which is still a var or rel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d5f70b08d2..3652768531 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -96,10 +96,8 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts -val is_unification_pattern_evar : env -> existential -> constr list -> - constr -> bool -val is_unification_pattern : env * int -> constr -> constr array -> - constr -> bool +val is_unification_pattern : env -> constr -> constr list -> + constr -> constr list option val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential |