diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cb478777f..97c636af7 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -60,6 +60,9 @@ val simple_cases_matrix_of_branches : val return_type_of_predicate : inductive -> int -> glob_constr -> predicate_pattern * glob_constr option +val subst_genarg_hook : + (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t + module PrintingInductiveMake : functor (Test : sig val encode : Libnames.reference -> Names.inductive |