aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r--kernel/nativecode.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4e78d2bd43..6b92474769 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -112,32 +112,32 @@ type symbol =
let get_value tbl i =
match tbl.(i) with
| SymbValue v -> v
- | _ -> anomaly "get_value failed"
+ | _ -> anomaly (Pp.str "get_value failed")
let get_sort tbl i =
match tbl.(i) with
| SymbSort s -> s
- | _ -> anomaly "get_sort failed"
+ | _ -> anomaly (Pp.str "get_sort failed")
let get_name tbl i =
match tbl.(i) with
| SymbName id -> id
- | _ -> anomaly "get_name failed"
+ | _ -> anomaly (Pp.str "get_name failed")
let get_const tbl i =
match tbl.(i) with
| SymbConst kn -> kn
- | _ -> anomaly "get_const failed"
+ | _ -> anomaly (Pp.str "get_const failed")
let get_match tbl i =
match tbl.(i) with
| SymbMatch case_info -> case_info
- | _ -> anomaly "get_match failed"
+ | _ -> anomaly (Pp.str "get_match failed")
let get_ind tbl i =
match tbl.(i) with
| SymbInd ind -> ind
- | _ -> anomaly "get_ind failed"
+ | _ -> anomaly (Pp.str "get_ind failed")
let symbols_list = ref ([] : symbol list)