diff options
| author | Matthieu Sozeau | 2014-09-17 20:51:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 20:51:40 +0200 |
| commit | f96dc97f48df5d0fdf252be5f28478a58be77961 (patch) | |
| tree | 5d741e02de71083b5e279121721dff7cb4b56516 /pretyping/patternops.ml | |
| parent | 17f68d403d248e899efbb76afeed169232946ecf (diff) | |
Fix bug #3593, making constr_eq and progress work up to
equality of universes, along with a few other functions in evd.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 4 |
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) -> |