diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
| commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
| tree | aefad2e3de35f75c46729f9310d33b56d3821961 /pretyping/evarutil.mli | |
| parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
| parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 49036798..f1d94b0a 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -206,6 +206,13 @@ val flush_and_check_evars : evar_map -> constr -> constr value of [e] in [sigma] is (recursively) used. *) val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds |