diff options
| author | letouzey | 2010-07-02 13:36:05 +0000 |
|---|---|---|
| committer | letouzey | 2010-07-02 13:36:05 +0000 |
| commit | 68a133db448e5663da6daf677d4d882bf1bad05c (patch) | |
| tree | aa3255a91f59ef9a2d7f5a9e9055165b6f5121be /plugins/extraction/common.mli | |
| parent | dacb4b76afe554f1a1e17d981bc98d9fc3a8e807 (diff) | |
Extraction: no more MPself hence no need for subst during pp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 6d33bd8ea0..33c14e33a5 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -43,7 +43,7 @@ val pp_global : kind -> global_reference -> string val pp_module : module_path -> string val top_visible_mp : unit -> module_path -val push_visible : module_path -> module_path option -> unit +val push_visible : module_path -> unit val pop_visible : unit -> unit val check_duplicate : module_path -> label -> string |