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 /interp/constrexpr_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 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index d857a5b60..687f5cb9e 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -82,6 +82,3 @@ val names_of_local_binders : local_binder list -> Name.t located list val names_of_local_assums : local_binder list -> Name.t located list (** Same as [names_of_local_binders], but does not take the [let] bindings into account. *) - -val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit) - -> Glob_term.glob_constr -> raw_cases_pattern_expr |