diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-28 09:22:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-28 09:22:25 +0000 |
| commit | 60d973e92c466a89410e359e4377ba5f4a7f0316 (patch) | |
| tree | aa90d242074037df177e31449af0f3d13ef1a60b /pretyping/evarutil.mli | |
| parent | afebe632272441db15ec0958825112e4558f7a85 (diff) | |
Diverses modifications autour de l'unification modulo conversion:
- extension de l'unification au cas de motifs (au sens de Dale Miller)
[appel de solve_pattern_eqn dans evar_conv_x],
- correction de bugs présumés dans real_clean et do_restrict_hyp
(prise en compte de la taille courante du contexte de de Bruijn),
- ajout d'une heuristique de beta-reduction de tete dans real_clean
(cf test-suite/success/unification.v),
- suppression de certains "try ... with _ => ...".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 6ce30ff79..2aceece0b 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -82,6 +82,9 @@ val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts +val is_unification_pattern : constr list -> bool +val solve_pattern_eqn : env -> constr list -> constr -> constr + (***********************************************************) (* Value/Type constraints *) |