aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.mli')
-rw-r--r--pretyping/pattern.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 4a477b8e5..cc36b260a 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -82,7 +82,7 @@ val is_matching :
increasing order based on the numbers given in the pattern *)
val matches_conv :
- env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
+ env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
(* To skip to the next occurrence *)
exception NextOccurrence of int
@@ -95,4 +95,4 @@ val sub_match :
up to conversion for constants in patterns *)
val is_matching_conv :
- env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool
+ env -> Evd.evar_map -> constr_pattern -> constr -> bool