From 29b7cd94ebf5587ab48b90dd15e39f2a9c1dd75c Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 27 Sep 2019 16:19:21 +0200 Subject: [PATCH] reindentation wrt 1.7.0 after rebase --- src/plugins/wp/MemRegion.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml index be5c827b90e..14660db121e 100644 --- a/src/plugins/wp/MemRegion.ml +++ b/src/plugins/wp/MemRegion.ml @@ -487,9 +487,9 @@ type loc = | Lfld of region * index * F.term * region overlay | Larr of region * index * F.term * F.term list * int * int list (* For Lxxx locations: - - index: start index inside the chunk - - term: additional shift index - - term list: array index from start *) + - index: start index inside the chunk + - term: additional shift index + - term list: array index from start *) (* -------------------------------------------------------------------------- *) (* --- Loc Basics --- *) -- GitLab