aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/perror.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/perror.ml')
-rw-r--r--contrib/correctness/perror.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 0435095fa..950bc62bf 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -16,10 +16,11 @@ open Names
open Term
open Himsg
-open Putil
open Ptype
open Past
+let is_mutable = function Ref _ | Array _ -> true | _ -> false
+let is_pure = function TypePure _ -> true | _ -> false
let raise_with_loc = function
| None -> raise