aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r--interp/constrintern.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b1bc63658..250871b9e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_gen : bool -> evar_map -> env ->
val intern_pattern : env -> cases_pattern_expr ->
Names.identifier list *
- ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
+ ((Names.identifier * Names.identifier) list * cases_pattern) list
val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list