From f7ae4e6433e44a0b3a838847c58ab72ffffa3d48 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Jul 2016 13:19:34 +0200
Subject: Some extra fixes in printing patterns in binders.

- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"

The question of whether or not to print the type of a binding pattern
by default seems open to me.
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 12da344623..6478ade61a 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -869,7 +869,7 @@ let rec match_iterated_binders islambda decls = function
       match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GLambda (_,na,bk,t,b) when islambda ->
       match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
-  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+  | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
       when not islambda && Id.equal p e ->
       match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
-- 
cgit v1.2.3