diff options
| author | herbelin | 2007-09-19 09:03:21 +0000 |
|---|---|---|
| committer | herbelin | 2007-09-19 09:03:21 +0000 |
| commit | b42da20a5b89a266b1a3964819d03b5ef7214688 (patch) | |
| tree | 2c543d38c98cbd4afbccf41b425bafee9f81bec9 /kernel/type_errors.mli | |
| parent | 5b67cba4b57102414c84a3df7255f980137855d9 (diff) | |
Indication de quel type de constantes est dépliable dans "simpl" (cf
message de Benjamin Pierce de sep 2007 sur coq-club) [report de la
révision 10128 de la 8.1 vers le trunk]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10129 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions