diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/declare.mli b/library/declare.mli index 9bbd0b8f40..345b3dc4e0 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -78,6 +78,8 @@ val constant_or_parameter_strength : constant_path -> strength val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable_path -> named_declaration * strength * sticky +val get_variable_with_constraints : + variable_path -> named_declaration * Univ.constraints * strength * sticky val variable_strength : variable_path -> strength val find_section_variable : identifier -> variable_path val last_section_hyps : dir_path -> identifier list |