Commit 12cc9195 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added missing hints.

parent 36b02cdc
......@@ -134,6 +134,8 @@ Parameter fill_spec :
\[ forall i, (i < ofs \/ ofs + len <= i) -> xs'[i] = xs[i] ]
).
Hint Extern 1 (RegisterSpec Array_ml.fill) => Provide fill_spec.
(* TEMPORARY todo: define [LibListZ.fill] at the logical level *)
(* -------------------------------------------------------------------------- *)
......@@ -155,6 +157,8 @@ Parameter iter_spec :
PRE ( t ~> Array xs \* I nil)
POST (# t ~> Array xs \* I xs ).
Hint Extern 1 (RegisterSpec Array_ml.iter) => Provide iter_spec.
(* TEMPORARY iter: give a stronger spec with "read" access to array *)
(* TEMPORARY give a generic spec to iter-like functions *)
......
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