diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /pretyping/glob_ops.mli | |
| 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/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 5195b98c8..1785c87be 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -18,7 +18,6 @@ open Locus open Glob_term (** Equalities *) -val glob_sort_eq : glob_sort -> glob_sort -> bool val cases_pattern_eq : cases_pattern -> cases_pattern -> bool |