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.

2 files changed, 4 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7476871890..e71daef999 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -848,10 +848,11 @@ and extern_local_binder scopes vars = function
   | (Inr p,bk,Some bd,ty)::l -> assert false
 
   | (Inr p,bk,None,ty)::l ->
-      let ty = extern_typ scopes vars ty in
+      let ty =
+        if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l)
+      (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
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 ->