diff options
| author | ppedrot | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /kernel/nativecode.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 12 |
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) |
