diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 14:57:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 14:57:58 +0000 |
| commit | 2040379ec1d79ff588498ca6f20d8c7b75d74533 (patch) | |
| tree | 030ab3eebf66961746ba164ca72a821a88d18851 /library/states.ml | |
| parent | 42088723410c0aef9767ee0cd18735eb081f05a6 (diff) | |
Préférence donnée aux constantes qui ne sont pas des projections
canoniques lors d'une unification constante/constante s'apprêtant à
déplier l'une des deux constantes (suggestion des utilisateurs de
structures canoniques), ceci afin de préserver des possibilités
ultérieures de résolution d'evars par équipement en structure
canonique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/states.ml')
0 files changed, 0 insertions, 0 deletions