From 8b2c4ea19c7930939c6d6d540558f042a60ac391 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 23:37:41 +0100
Subject: Making structure of type "tolerability" and related clearer.

Also renamed it to relative_entry_level.

Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused

Should not change global semantics (except error message in pr_arg).
---
 plugins/ltac/extraargs.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/extraargs.mlg')

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index bab6bfd78e..5835d75c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -298,7 +298,7 @@ END
 let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t)
 
 }
 
-- 
cgit v1.2.3