diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-21 15:24:51 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-21 15:24:51 +0000 |
| commit | 3e5f0e1521168412e3f0982a6c5456fd2978e63b (patch) | |
| tree | be4a75f0d8371ea398533150b4fffb82a38fc94f /kernel/entries.ml | |
| parent | cfa3aa27f1141fe732a473efd0cff794694c63bb (diff) | |
Removed some useless code in mod_typing that was redundant with safe_typing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 8bb616d8b..fb134b1c7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -79,7 +79,6 @@ type specification_entry = and module_type_entry = MTEident of kernel_name | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry - | MTEsig of mod_self_id * module_signature_entry | MTEwith of module_type_entry * with_declaration and module_signature_entry = (label * specification_entry) list @@ -91,7 +90,6 @@ and with_declaration = and module_expr = MEident of module_path | MEfunctor of mod_bound_id * module_type_entry * module_expr - | MEstruct of mod_self_id * module_structure | MEapply of module_expr * module_expr and module_structure = (label * specification_entry) list |