aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Splitting.ml
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
committerJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
commit5664fddcab15ef4482d583673c75e07bd1e96d0a (patch)
tree878b22860e69405ba5cf6fd2798731dac8ce660c /backend/Splitting.ml
parentb960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff)
parentfe73ed58ef80da7c53c124302a608948fb190229 (diff)
downloadcompcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz
compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip
Merge remote-tracking branch 'origin/master' into parser_fix
Diffstat (limited to 'backend/Splitting.ml')
-rw-r--r--backend/Splitting.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 97b26a50..17b8098d 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -39,9 +39,9 @@ let rec repr lr =
| Link lr' -> let lr'' = repr lr' in lr.kind <- Link lr''; lr''
| _ -> lr
-let same_range lr1 lr2 =
- lr1 == lr2 || (* quick test for speed *)
- repr lr1 == repr lr2 (* the real test *)
+let same_range lr1 lr2 =
+ lr1 == lr2 || (* quick test for speed *)
+ repr lr1 == repr lr2 (* the real test *)
let unify lr1 lr2 =
let lr1 = repr lr1 and lr2 = repr lr2 in