diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-24 17:03:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-24 17:03:28 +0000 |
| commit | 479c522938fea2fdc4281123c3e0581551f955a8 (patch) | |
| tree | f4583ccd46c39a50dea678b37bf2d659bca76a0d /pretyping/recordops.ml | |
| parent | a0726f4ae896bb668d4da4c96501686b25cd82cd (diff) | |
Morceau de code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9082 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5fffeb709..fa3a61afc 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -78,7 +78,7 @@ let (inStruc,outStruc) = discharge_function = discharge_structure; export_function = (function x -> Some x) } -let declare_structure (s,c,_,kl,pl) = +let declare_structure (s,c,kl,pl) = Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) let lookup_structure indsp = Indmap.find indsp !structure_table |