aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native
diff options
context:
space:
mode:
authorQuentin Garchery <garchery.quentin@gmail.com>2018-10-27 18:08:53 +0200
committerValentin Blot <24938579+vblot@users.noreply.github.com>2018-10-27 18:29:50 +0200
commit4e6129afb9aab53d14f16ac74a5a4e80323b5813 (patch)
tree7037708e3ae50407842b8216117d0edb47e71c60 /src/versions/native
parenta2e8b2f68fa82ca96468cb0613710c07b27192da (diff)
downloadsmtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.tar.gz
smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.zip
formatting
Diffstat (limited to 'src/versions/native')
-rw-r--r--src/versions/native/structures.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 42e5792..8db91fd 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -60,7 +60,7 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
if r1 <> 0 then (
let traceq = Array.make (r1 + 1) def_step in
for i = 0 to r1-1 do
- r := next !r;
+ r := next !r;
traceq.(i) <- step_to_coq !r;
done;
trace.(q) <- mkArray (step, traceq)