diff options
| author | Pierre-Marie Pédrot | 2015-02-23 11:08:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-23 11:08:27 +0100 |
| commit | 95d1ba0636d95e213f327fc9dba9002b29e95da6 (patch) | |
| tree | fa70e88054365c1bd97976ee64199ef36021f441 /dev | |
| parent | f1389e10e6bf15e0fe3fd120f4aa8e59579a16b4 (diff) | |
| parent | f7dfa9d5e1195b8db3711126f953c1605e8cfcf2 (diff) | |
Merge branch 'v8.5'
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 |