aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r--pretyping/cases.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index cbf5788e4..327ee0015 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -124,7 +124,7 @@ val prepare_predicate : ?loc:Loc.t ->
(types * tomatch_type) list ->
(rel_context * rel_context) list ->
constr option ->
- glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+ glob_constr option -> (Evd.evar_map * Name.t list * constr) list
-val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map