diff options
| author | letouzey | 2007-10-09 20:04:06 +0000 |
|---|---|---|
| committer | letouzey | 2007-10-09 20:04:06 +0000 |
| commit | bfa770fa6077dee42d734232908cd5631feb6af6 (patch) | |
| tree | 56c23f6fbd17e9bac3f47373e1c7860c5a76817d /contrib/extraction/table.mli | |
| parent | 1a63e12d7d3612f92ba72884eb7dd9083c2dec3c (diff) | |
Extract Inline/Inductive/Constant can now be used from inside a module
It even seems to work from inside a functor. Fix old bug #472.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10204 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index cc793b1a1c..7bd2297cdf 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -28,7 +28,6 @@ val error_unknown_module : qualid -> 'a val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_unqualified_name : string -> string -> 'a val error_MPfile_as_mod : dir_path -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit |