diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 15:51:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 15:51:20 +0200 |
| commit | a0da3a68d12141ba226ce94027b90a01389099d0 (patch) | |
| tree | 418ccf3d1b723555bd45ecb647823a5af851097e /printing/ppconstr.mli | |
| parent | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff) | |
| parent | a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f (diff) | |
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1f1308b0d..127c4471c 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,8 +41,8 @@ val pr_name : Name.t -> Pp.t val pr_qualid : qualid -> Pp.t val pr_patvar : patvar -> Pp.t -val pr_glob_level : glob_level -> Pp.t -val pr_glob_sort : glob_sort -> Pp.t +val pr_glob_level : Glob_term.glob_level -> Pp.t +val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> lident option * recursion_order_expr -> |