diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8695d52b12..425fd5096e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -37,7 +37,7 @@ val print_allow_match_default_clause : bool ref val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern -val subst_glob_constr : substitution -> glob_constr -> glob_constr +val subst_glob_constr : env -> substitution -> glob_constr -> glob_constr val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g |