diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index c16b4abbac..80eaa6b850 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -126,6 +126,7 @@ Ppextend Pputils Genarg Stdarg +Constrarg Constrexpr_ops Notation_ops Topconstr diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f59c300a9e..a9b942e7bb 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -409,6 +409,7 @@ END open Pcoq open Genarg +open Constrarg open Egramml let _ = |