diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:31:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:31:34 +0200 |
| commit | 6390887ce1fd32c2180f373f1e701d9488c341f9 (patch) | |
| tree | ef53b4077d1b947f7f3064765fa8a609efbb5cab /checker/univ.mli | |
| parent | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (diff) | |
Remove unused substitution functions in checker.
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 27f4c9a6e..89dd64486 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -197,19 +197,12 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe -(** Make a universe level substitution: the instances must match. *) -val make_universe_subst : Instance.t -> universe_context -> universe_level_subst -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_level_subst -> universe_context -> constraints - (** Level to universe substitutions. *) val is_empty_subst : universe_subst -> bool 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 |