diff options
| author | Pierre Letouzey | 2016-05-30 17:16:25 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-05-30 17:16:25 +0200 |
| commit | 991188b16cc963ea4f8e49075c90eb312c6fe143 (patch) | |
| tree | ac8563ab63395841e2773f5e1c5b7b82a2261dab /plugins/extraction/table.ml | |
| parent | b445ebb0f511ab3be11d602fe091a0bc5f1ad883 (diff) | |
Extraction : add a location in the error message about polyprop
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 466c8054b8..f336941ee3 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -391,9 +391,15 @@ let error_no_module_expr mp = ++ str "some Declare Module outside any Module Type.\n" ++ str "This situation is currently unsupported by the extraction.") -let error_singleton_become_prop id = +let error_singleton_become_prop id og = + let loc = + match og with + | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++ + str " (or in its mutual block)" + | None -> mt () + in err (str "The informative inductive type " ++ pr_id id ++ - str " has a Prop instance.\n" ++ + str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ str "The Ocaml extraction cannot handle this situation yet.\n" ++ |