diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 15:21:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 15:21:10 +0200 |
| commit | 9a82982c1eb8cb1d6a61d3d497d669591fb68747 (patch) | |
| tree | 946bacf9494795d8cfb34f633630bdab13feaa76 /doc/refman/RefMan-ind.tex | |
| parent | 29844f673b5af1b0e50efc7b41cf5660d0a37d03 (diff) | |
Fixing #3657 (check that both sides of a "change with" have the same
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
Diffstat (limited to 'doc/refman/RefMan-ind.tex')
0 files changed, 0 insertions, 0 deletions