diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ab9393915..cad5551c1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -67,14 +67,14 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 let encode_bool r = let (x,lc) = encode_inductive r in if not (has_two_constructors lc) then - user_err ~loc:(loc_of_reference r) "encode_if" + user_err ~loc:(loc_of_reference r) ~hdr:"encode_if" (str "This type has not exactly two constructors."); x let encode_tuple r = let (x,lc) = encode_inductive r in if not (isomorphic_to_tuple lc) then - user_err ~loc:(loc_of_reference r) "encode_tuple" + user_err ~loc:(loc_of_reference r) ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); x |