diff options
| author | Maxime Dénès | 2017-07-17 07:35:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-17 07:35:10 +0200 |
| commit | f7fda5a7e2b43e3ac24d0a2a5c5e4a7b9cda4bdd (patch) | |
| tree | 37b164963d8ca7e4899a53278a6d2ee654c9b455 /dev/include | |
| parent | a14a894870b9503e649bb79f32a26a6b9171f02a (diff) | |
| parent | 0e8fc03878b360e540069df139cbcc278837d5d2 (diff) | |
Merge PR #874: Adding econstr printer to "include" file.
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 31ae5da71a..0d34595f4f 100644 --- a/dev/include +++ b/dev/include @@ -31,6 +31,7 @@ #install_printer (* glob_constr *) ppglob_constr;; #install_printer (* open constr *) ppopenconstr;; #install_printer (* constr *) ppconstr;; +#install_printer (* econstr *) ppeconstr;; #install_printer (* constr_substituted *) ppsconstr;; #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; |