diff options
| author | Pierre Letouzey | 2016-05-30 17:16:25 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-05-30 17:25:22 +0200 |
| commit | cb31cd671a0ef4da0cf834dad5b67776098bb0d1 (patch) | |
| tree | a8cd948a0377602c71116f4a1bffd366102d7b32 /plugins/extraction/table.ml | |
| parent | 35fb7ad402fee1e3e247ccf37438d3a7a5230629 (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 d7842e127d..5f83d2949e 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" ++ |