diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-31 23:05:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-31 23:17:47 +0200 |
| commit | ce029533a1f0fc6ac9e28d162350a64446522246 (patch) | |
| tree | bb85295b8e8141db8494ed03002e17c9e713eed5 /engine/evarutil.mli | |
| parent | 6add354ad9ca0f68d3ef311c4e53ee96d9fdb4d7 (diff) | |
Make the Constr.kind_of_term type parametric in sorts and universes.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index da49d4e11..ca9591e71 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -178,7 +178,8 @@ val flush_and_check_evars : evar_map -> constr -> Constr.constr (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the value of [e] in [sigma] is (recursively) used. *) -val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr,Constr.types) kind_of_term +val kind_of_term_upto : evar_map -> Constr.constr -> + (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable |