aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 54ce29bf71..44ff2b5b8c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -75,8 +75,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) =
and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
Array.equal Name.equal n1 n2 &&
- Array.equal eq_constr c1 c2 &&
- Array.equal eq_constr r1 r2
+ Array.equal Term.eq_constr c1 c2 &&
+ Array.equal Term.eq_constr r1 r2
let rec occur_meta_pattern = function
| PApp (f,args) ->