From de7d2fdb97975dcd94005bb6fa79a312c8afa017 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 28 Oct 2017 20:07:44 +0200
Subject: Fixing #5401 (printing of patterns with bound anonymous variables).

This fixes also #5731, #6035, #5364.
---
 pretyping/patternops.ml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3b3ad021e4..aaa9467068 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -96,6 +96,31 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
+let rec occurn_pattern n = function
+  | PRel p -> Int.equal n p
+  | PApp (f,args) ->
+      (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
+  | PProj (_,arg) -> occurn_pattern n arg
+  | PLambda (na,t,c)  -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+  | PProd (na,t,c)  -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+  | PLetIn (na,b,t,c)  ->
+     Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t ||
+     (occurn_pattern (n+1) c)
+  | PIf (c,c1,c2)  ->
+      (occurn_pattern n c) ||
+      (occurn_pattern n c1) || (occurn_pattern n c2)
+  | PCase(_,p,c,br) ->
+      (occurn_pattern n p) ||
+      (occurn_pattern n c) ||
+      (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+  | PMeta _ | PSoApp _ -> true
+  | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+  | PVar _ | PRef _ | PSort _ -> false
+  | PFix fix -> not (noccurn n (mkFix fix))
+  | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+
+let noccurn_pattern n c = not (occurn_pattern n c)
+
 exception BoundPattern;;
 
 let rec head_pattern_bound t =
-- 
cgit v1.2.3