diff options
| author | herbelin | 2008-02-07 21:49:05 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-07 21:49:05 +0000 |
| commit | 62091e13412cce60ca32aba542b146f0fe8403e1 (patch) | |
| tree | 13f5e42841568f01548f0d08332d4823456cb66e /dev/include | |
| parent | 3c9fe09ad4cdba24b906658cb14df0b44ed634a2 (diff) | |
Mise en place d'une toute petite amélioration de l'unification de
apply : si on a trouvé une méta, alors, on l'utilise pour instancier
les trous lors de la tentative de conversion modulo delta. Cela permet
ainsi de résoudre de petits cas d'unification, tel que celui annoncé
échouant dans le "beginner question" du 6 fevrier 2008 de coq-club.
Solde au passage de modifs cosmétiques de setoid_replace.ml avant
abandon probable du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions