diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 34f10b31ab..5a913a9067 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -118,15 +118,32 @@ val debug_pr_delta : delta_resolver -> Pp.std_ppcmds val subst_mp : substitution -> module_path -> module_path -val subst_ind : +val subst_mind : substitution -> mutual_inductive -> mutual_inductive +val subst_ind : + substitution -> inductive -> inductive + +val subst_pind : substitution -> pinductive -> pinductive + val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : + substitution -> pconstant -> constant * constr + +val subst_pcon : + substitution -> pconstant -> pconstant + +val subst_pcon_term : + substitution -> pconstant -> pconstant * constr + +val subst_con_kn : substitution -> constant -> constant * constr +val subst_constant : + substitution -> constant -> constant + (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" |