diff options
| author | herbelin | 2000-12-19 15:44:47 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-19 15:44:47 +0000 |
| commit | deadd9eb4dd81b193ab93c571a6b39b6843c5687 (patch) | |
| tree | 3ab4059ec3c947a77851b3fca87c8365ce4f8c2c /kernel/type_errors.mli | |
| parent | 94236aaad5f951ff5d47d9c1f63250081da4607a (diff) | |
Export fonction testant si un inductive est un record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions