diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 13:55:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 13:55:20 +0000 |
| commit | 72e450d7ef0f01f2f92ce0089885f071d75cc74d (patch) | |
| tree | 6fbc5c8005bfe158aa423c1b94f812f22450b20b /library/goptions.ml | |
| parent | 71df2a928fb9367a632a6869306626e3a5c7a971 (diff) | |
print_id, print_sp -> pr_id, pr_sp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 64b08f6f4..dc5f994e3 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -340,7 +340,7 @@ let msg_sync_option_value (name,v) = | BoolValue false -> [< 'sTR "false" >] | IntValue n -> [< 'iNT n >] | StringValue s -> [< 'sTR s >] - | IdentValue id -> [< print_id id >] + | IdentValue id -> [< pr_id id >] let msg_async_option_value (name,vref) = match vref with |