diff options
| author | Matthieu Sozeau | 2014-04-28 13:47:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 902da7d2949464ff54dafc3fda1d44365270d2e1 (patch) | |
| tree | e8af894bb79090b316df4fbd247e09fb464bd2ac /pretyping/evarutil.mli | |
| parent | 6869b22e2546b69acb74e18dc491029897ba36a3 (diff) | |
Try a new way of handling template universe levels
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 b860ce3370..d197ad2efe 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -216,3 +216,10 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a + +(* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *) +val get_template_constructor_type : evar_map ref -> constructor -> int -> + (Univ.universe option list * types) + +val get_template_inductive_type : evar_map ref -> inductive -> int -> + (Univ.universe option list * types) |