diff options
Diffstat (limited to 'vernac/declareUniv.mli')
| -rw-r--r-- | vernac/declareUniv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index e4d1d5dc65..ca990a58eb 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val do_universe : poly:bool -> lident list -> unit -val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit +val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit |