diff options
| -rw-r--r-- | vernac/metasyntax.ml | 16 |
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()) ++ |