From 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 5 Sep 2014 20:27:37 +0200 Subject: Fix checker treatment of inductives using subst_instances instead of subst_univs_levels. --- checker/univ.mli | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'checker/univ.mli') diff --git a/checker/univ.mli b/checker/univ.mli index b2f2c9c18..27f4c9a6e 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -18,6 +18,7 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val equal : t -> t -> bool end type universe_level = Level.t @@ -122,7 +123,7 @@ val check_constraints : constraints -> universes -> bool (** {6 Support for old-style sort-polymorphism } *) val subst_large_constraints : - (universe * universe) list -> universe -> universe + (universe_level * universe) list -> universe -> universe (** {6 Support for universe polymorphism } *) @@ -209,6 +210,19 @@ val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> universe -> universe val subst_univs_constraints : universe_subst_fn -> constraints -> constraints + +(** Substitution of instances *) +val subst_instance_instance : universe_instance -> universe_instance -> universe_instance +val subst_instance_universe : universe_instance -> universe -> universe +val subst_instance_constraints : universe_instance -> constraints -> constraints + +(* val make_instance_subst : universe_instance -> universe_level_subst *) +(* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) + +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_context -> universe_context +val instantiate_univ_constraints : universe_instance -> universe_context -> constraints + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds -- cgit v1.2.3