diff options
| author | Pierre Letouzey | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /pretyping/patternops.ml | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a2e8e45996..cc13d342a5 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 -| PSort s1, PSort s2 -> glob_sort_eq s1 s2 +| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 |