diff options
| author | herbelin | 2006-08-28 09:22:25 +0000 |
|---|---|---|
| committer | herbelin | 2006-08-28 09:22:25 +0000 |
| commit | 60d973e92c466a89410e359e4377ba5f4a7f0316 (patch) | |
| tree | aa90d242074037df177e31449af0f3d13ef1a60b /kernel/make-opcodes | |
| 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 'kernel/make-opcodes')
0 files changed, 0 insertions, 0 deletions