From 7002b3daca6da29eadf80019847630b8583c3daf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 3 Aug 2014 20:02:49 +0200 Subject: Move to a representation of universe polymorphic constants using indices for variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside. --- kernel/vars.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'kernel/vars.mli') diff --git a/kernel/vars.mli b/kernel/vars.mli index 0d5ab07db..cfa9fcb26 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -83,3 +83,7 @@ val subst_univs_constr : universe_subst -> constr -> constr val subst_univs_level_constr : universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context + +(** Instance substitution for polymorphism. *) +val subst_instance_constr : universe_instance -> constr -> constr +val subst_instance_context : universe_instance -> rel_context -> rel_context -- cgit v1.2.3