diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:04 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:04 +0000 |
| commit | cb14f24943415cce8fcbf36cb7cdd87d27c60628 (patch) | |
| tree | bef70da7ddc397c644001b299a9534e4081b078f /kernel/mod_typing.mli | |
| parent | 7c907ade730d47dfa0a39a95be5dcfb422f9d553 (diff) | |
Safe_typing: some refactoring (avoiding copy-paste of record definitions)
Many of the record definitions for new safe_environment follow
the same pattern, we factorize them in a generic add_field function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_typing.mli')
0 files changed, 0 insertions, 0 deletions