Preparing to simplifying the structure of type "tolerability".

The "Any" case was not reached formerly for ETPattern and ETConstr as
far as I can see. So there should be no change of semantics.

1 files changed, 7 insertions, 9 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 69d9bd4c41..3bfa5cb683 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -745,15 +745,13 @@ let recompute_assoc typs = let open Gramlib.Gramext in
 
 let pr_arg_level from (lev,typ) =
   let pplev = function
-  | (n,L) when Int.equal n from -> str "at next level"
-  | (n,E) -> str "at level " ++ int n
-  | (n,L) -> str "at level below " ++ int n
-  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
-  | (n,_) -> str "Unknown level" in
-  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
-  (match typ with
-   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
-   | _ -> mt ())
+  | (n,L) when Int.equal n from -> spc () ++ str "at next level"
+  | (n,E) -> spc () ++ str "at level " ++ int n
+  | (n,L) -> spc () ++ str "at level below " ++ int n
+  | (n,Prec m) when Int.equal m n -> spc () ++ str "at level " ++ int n
+  | (n,Prec _) -> assert false
+  | (n,Any) -> mt () in
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
 
 let pr_level ntn (from,fromlevel,args,typs) =
   (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++