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 /tactics/setoid_replace.mli | |
| 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 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index ecad6a574e..2dd153b3ff 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -79,3 +79,5 @@ val new_named_morphism : val relation_table_find : constr -> relation val relation_table_mem : constr -> bool + +val prrelation : relation -> Pp.std_ppcmds |