diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-22 11:21:13 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-22 11:21:13 +0000 |
| commit | 9cdb1ac910568e3110da9a47c4dec4708cef858b (patch) | |
| tree | 4ff091a7346ef5bc6249b4d98ab8aaa35c8337cf /dev | |
| parent | e1b02cbf1c18e5ebc5087a8e1f40c9d8534f69a0 (diff) | |
Ajout d'un warning losrqu'un nom de bibliothèque est ambigü
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions