Commit 98b873ee authored by charguer's avatar charguer
Browse files

renaming arraymap

parent f4bca762
Set Implicit Arguments.
Require Import UF.
Require Import ArrayMap.
Import ArrayMap.
Require Import UFArray_ml.
Implicit Type P : map int int.
......@@ -18,7 +18,7 @@ Implicit Types t : loc.
indexed in the range [0...(n-1)]. *)
Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Hexists (P:map int int), t ~> MArray P
Hexists (P:map int int), t ~> ArrayMap P
\* \[conseq_dom n P /\ roots P R].
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment