From 277d5c0d56e7ba79bd338e50e15bc3c6cb62fb65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 28 Mar 2018 20:18:18 +0200
Subject: Getting rid of some false "collision between bound variable names"
 warnings.

- In a situation like "match x with ... end" with no "return" clause
  we don't warn for the implicit "as x" coming from repeating "x"
- In a multiple fixpoint, we don't warn for the recursive context
  being distributed several times over the different mutual
  components.
---
 pretyping/glob_ops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 74f2cefab6..aa3d246f8a 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -247,8 +247,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
     let fold_tomatch (v',acc) (tm,(na,onal)) =
-      (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
-                        (Name.fold_right g na v') onal,
+      ((if rtntypopt = None then v' else
+       Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
+                        (Name.fold_right g na v') onal),
        f v acc tm) in
     let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
     let acc = Option.fold_left (f v') acc rtntypopt in
@@ -259,6 +260,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GIf (c,rtntyp,b1,b2) ->
     f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
   | GRec (_,idl,bll,tyl,bv) ->
+    let v' = Array.fold_right g idl v in
     let f' i acc fid =
       let v,acc =
 	List.fold_left
@@ -266,7 +268,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
             (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
           (v,acc)
           bll.(i) in
-      f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+      f v' (f v acc tyl.(i)) (bv.(i)) in
     Array.fold_left_i f' acc idl
   | GCast (c,k) ->
     let acc = match k with
-- 
cgit v1.2.3