diff options
| author | Pierre-Marie Pédrot | 2015-02-19 17:48:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-19 19:08:54 +0100 |
| commit | 97e5a748bf921dc6cefae0041d2adb00f24f34cb (patch) | |
| tree | 44c44d2dbd4c5dd5116f2ce7fa3df964a7a3da54 /dev | |
| parent | ff26623a0b847149e6f119c98b7564d92710d59a (diff) | |
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 650897ef74..f969f01329 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -502,7 +502,7 @@ open Egramml let _ = try - Vernacinterp.vinterp_add ("PrintConstr", 0) + Vernacinterp.vinterp_add false ("PrintConstr", 0) (function [c] when genarg_tag c = ConstrArgType && true -> let c = out_gen (rawwit wit_constr) c in @@ -519,7 +519,7 @@ let _ = let _ = try - Vernacinterp.vinterp_add ("PrintPureConstr", 0) + Vernacinterp.vinterp_add false ("PrintPureConstr", 0) (function [c] when genarg_tag c = ConstrArgType && true -> let c = out_gen (rawwit wit_constr) c in |