diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 45ea77d13..6b2e206b6 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -18,12 +18,12 @@ open Ppextend open Topconstr open Term open Pattern -open Glob_term open Constrextern open Termops open Decl_kinds open Misctypes open Locus +open Genredexpr (*i*) let sep_v = fun _ -> str"," ++ spc() |