diff options
| author | ppedrot | 2012-12-18 17:09:31 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-18 17:09:31 +0000 |
| commit | aa37087b8e7151ea96321a11012c1064210ef4ea (patch) | |
| tree | fff9ed837668746545832e3bd9f0a6dd99936ee4 /plugins/extraction/extraction.ml | |
| parent | f61e682857596f0274b956295efd2bfba63bc8c0 (diff) | |
Modulification of Label
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index b892ae57a5..5ab3647d67 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | Anonymous::l, typ::typs -> None :: (select_fields l typs) | Name id::l, typ::typs -> - let knp = make_con mp d (label_of_id id) in + let knp = make_con mp d (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((=) Keep) (type2signature env typ) then projs := Cset.add knp !projs; |