aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.mli')
-rw-r--r--pretyping/evarutil.mli7
1 files changed, 0 insertions, 7 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 55171eb4c..c0708aa85 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -221,10 +221,3 @@ 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_level option list * types)
-
-val get_template_inductive_type : evar_map ref -> inductive -> int ->
- (Univ.universe_level option list * types)