diff options
| author | herbelin | 2006-09-30 17:34:31 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-30 17:34:31 +0000 |
| commit | 3dc4e18383e8556f1e33b9295ee348fe145cfcbf (patch) | |
| tree | d3cc0adeecedfa7b5c523009330394d33266b15f /pretyping/inductiveops.mli | |
| parent | 7cd945fb3db868bc28d4c0dce101b03b2de9ffe3 (diff) | |
Suppression de la comparaison (inutile) des paramètres globaux des
constructeurs dans la recherche des positions de divergence entre
expressions construites (possible source d'inefficacité
d'injection/discriminate dans le cas de paramètres globaux
convertibles mais syntaxiquement distincts -- cf rapport de bug 1173,
première suggestion, même si dans le cas soumis les paramètres sont
syntaxiquement les mêmes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9193 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/inductiveops.mli')
0 files changed, 0 insertions, 0 deletions